Formal Methods Laboratory

We defined a more constructive mathematics for experimental sciences, named Finitely Supported Mathematics (FSM) [B1] which deals with a more relaxed notion of infiniteness. Informally, in Finitely Supported Mathematics we can model infinite structures by using only a finite number of characteristics. More precisely, in FSM we admit the existence of infinite structures, but for an infinite structure we prove that only of a finite family of its elements is “really important” in order to characterize the related structure, whilst the other elements are somehow “similar”. This means that we associate to each object a finite family of elements characterizing it, which is called “finite support”. FSM has strong connections with the Fraenkel-Mostowski (FM) permutative model of Zermelo-Fraenkel set theory with atoms (ZFA), with Fraenkel-Mostowski axiomatic set theory, with the theory of nominal sets, and with the theory of generalized nominal sets. More exactly, FSM represents a reformulation of the classical Zermelo-Fraenkel algebra in terms of finitely supported structures, where the set of atoms should be infinite (but not necessary countable as in the theory of nominal sets). The principles of constructing FSM have historical roots both in the definition of logical notions by Alfred Tarski and in the Erlangen Program of Felix Klein for the classification of various geometries according to invariants under suitable groups of transformations. We have also presented several similarities between FSM, admissible sets introduced by Barwise and Gandy machines.

We defined a theory of abstract interpretations in the framework of invariant sets [L1] by translating the notions of lattices and Galois connections into this framework, and presenting their properties in terms of finitely supported objects. We introduced the notions of invariant correctness relation and invariant representation function and we establish the relationship between these notions and invariant Galois connections. We also presented specific techniques for approximating the minimal fixed points of finitely supported transition functions.

For an invariant group, we defined the notion of finitely supported subgroup [L2], and we presented some algebraic properties of these subgroups. We prove that the family of all finitely supported subgroups of an invariant group forms an invariant complete lattice and an invariant algebraic domain.

We studied generalized multisets (multisets that allow possible negative multiplicities) [L3] both in the Zermelo-Fraenkel framework and in FSM. We extended the notion of generalized multiset over a finite alphabet, and we replaced it by the notion of algebraically finitely supported generalized multiset over a possibly infinite alphabet. We analyzed the correspondence between some properties of generalized multisets obtained in FSM where only finitely supported objects are allowed, and those obtained in the classical Zermelo-Fraenkel framework.

We defined a transformation of membrane systems, possibly with promoter/inhibitor rules, priority relations, and membrane dissolution, into formulas of the chemical calculus such that terminating computations of membranes correspond to terminating reduction sequences of formulas and vice versa [L4]. This means that the same result can be extracted from the underlying computations of the two types of systems.

We defined a translation of the spiking neural P systems with weighted synapses into a class of timed safety automata, proving that such a translation is formally correct [L5]. This relationship allows the verification of several kinds of properties, both qualitative and quantitative, using tools and techniques developed for timed automata.

After we recently considered the possibility of using bio-inspired mobility for solving a weak NP-complete problem (Partition), in [L6] we provided a semi-uniform polynomial solution for a strong NP-complete problem (Bin Packing) by means of membrane computing techniques. The solution employs mobile membranes and elementary membrane division.

We studied the safety of car control systems in which vehicle-to-vehicle interactions are described in a modular and compositional manner [L7]. Such a description simplifies a complex verification process, which involves control decisions regarding acceleration, deceleration, lane switching and braking distance. We focused on the problem of adjusting vehicle speed in order to maintain a proper distance between vehicles on the same lane. The components of the control system are represented as processes in the process algebra Communicating Sequential Processes, and the compositional parallel operator is used to describe the whole system. Safety properties are formally verified by employing the Concurrency Workbench of the New Century tool.

We investigated a language similar to a process algebra introduced by Cardelli for DNA computing [L8]. For such a language, we defined a new denotational semantics by using complete metric spaces, in which various semantic functions are defined as fixed points of appropriate higher-order mappings. We compared this denotational semantics with an operational semantics and establish a formal relationship between them by using an abstraction operator and a fixed point argument. In this way, we proved the correctness of the denotational semantics with respect to the operational one.

We developed a theory of abstract interpretations which is consistent with the principles of constructing Finitely Supported Mathematics (FSM) [L9]. We had translated the notions of lattices and Galois connections into FSM, and then we presented their properties in terms of invariant or finitely supported relations. We presented the notions of invariant correctness relation and invariant representation function internally in the new context FSM, we emphasized an equivalence between them, and we established an FSM relationship between these notions and invariant Galois connections. We provided some widening and narrowing techniques in order to approximate the least fixed points of finitely supported transition functions.

We proposed a mobility type system for description and verification of distributed systems in which processes are asked to move between locations where important local interactions are required [L10]. We used a simple version of distributed pi-calculus to define mobility types. The novelty of this approach is that we pointed out sequences of migrations as global types, and investigated scenarios in which processes are required to follow such a sequence of migrations along several locations. The typing system ensures certain properties including type soundness.

We translated a restricted variant of the stochastic spiking neural P systems using uniform distribution into a network of timed automata, proving that such a translation preserves faithfully their behaviours [L11]. This relationship allows the verification of several kinds of properties (both qualitative and quantitative) using the statistical model checking extension of the complex software tool Uppaal.

Starting from the calculus of structures we made a behavioural analysis of sessions [L12]. The approach involves specifications of global and local sessions inspired by the Scribble language. The calculus features a novel operator that synchronises parts of a protocol that must be treated atomically. Firstly, the calculus can be used to determine whether local sessions can be compose in a type safe fashion such that sessions are capable of successfully completing. Secondly, the calculus defines a subtyping relation for sessions that allows causal dependencies to be weakened while retaining termination potential. Consistency and complexity results follow from proof theory.

We defined, using the calculus of structures, an expressive but decidable first-order system (named MAV1) [L13,L14]. In addition to first-order universal and existential quantifiers the system incorporates a pair of nominal quantifiers called `new' and `wen', distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these operators is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkeeping enables private names to be modelled as predicates in MAV1.In this way we have the advantage that linear implication defines a precongruence over processes that fully respects causality and branching. The transitivity of this precongruence is established by novel techniques for handling first-order quantifiers in the cut elimination proof.

In [L15] we introduced the notion of countable set in FSM. We proved some algebraic properties of FSM countable sets, and we established several relationship results between countable union theorems and countable choice principles in FSM.

In [L16] we made a presentation of the principles of constructing FSM and of the general methods for proving that a certain structure is finitely supported. More exactly, we described the constructive method for defining the support of an algebraic structure, the equivariance principle in higher order logic and the S-support principle in higher order logic. We also analyzed the consistency of various choice principles in FSM.

We defined a hierarchical nested system together with a multiset-based type system involving a ratio control of the resources [L17]. This ratio control keeps the resources between lower and upper thresholds. According to a typed semantics, each rule of the system can be applied only if the left-hand side term of the rule is well-typed. A type inference is defined for d educing the type of each term of such a system. Soundness and completeness results are proved for this type inference.

We proved that an abstract model of protein-protein interaction [L18] derived from membrane computing has the same computational power as a Turing machine by using a rather small number of proteins having at most length two, where length is an abstract measure of complexity.