Formal Methods Laboratory

We introduced and studied nominal groups, providing some algebraic properties of them [L1]. We focused on the properties of nominal homomorphisms, and studied the correspondence between some results obtained in the Fraenkel-Mostowski framework and those obtained in the classical Zermelo-Fraenkel framework.

We formally expressed and gave an implementation of mobile ambients, a formalism for describing mobility in distributed systems, into temporal logic of actions, a logic for specifying and verification concurrent systems [L2].

We presented generalized multisets [L3] in the Zermelo-Fraenkel framework, in Reverse Mathematics and proved that the set of all generalized multisets over a certain finite set is a finitely-generated, lattice-ordered, free abelian group. In the Fraenkel-Mostowski framework, we studied their nominal properties.

Inspired by the functioning of the sodium-potassium pump, we introduced and studied a threshold-based type system in a bio-inspired rewriting formalism [L4]. Such a system can avoid errors in the definition of the formal model used to model and verify certain biologic processes. For this type system we prove a subject reduction theorem, together with soundness and completeness theorems. We also presented a type inference for deducing the type of a system [L12].

We defined a real-time extension of P systems, a multiset rewriting system, in which each membrane and each object has a lifetime attached to it, and we used these lifetimes to define and study various behavioural equivalences [L5]. We also established sufficient conditions for guaranteeing progression over time.

We presented TiMo, a simple and expressive formalism, that is a simplified version of timed distributed pi-calculus [L6]. TiMo aims to bridge the gap between the existing theoretical approach of process calculi and forthcoming realistic languages for multi-agent systems. We developed a general framework for reasoning about systems specified using TiMo [L11]. We use the Event-B modelling method as the target for translating TiMo specifications. Subsequently, we utilised the supporting Rodin platform of Event-B to verify system properties using the embedded theorem-provers and model checkers. The main feature of our encoding include a generic model capturing the syntax and semantics of TiMo, together with a concrete model corresponding to each specific TiMo specification. We notice that this paper has received the „Best Paper Award” at the rank A conference ICECCS 2014.

Operational models, such as labelled transition systems, tend to assume an interleaving semantics, which serialises transactions. To address this limitation, we provided an operational model that allows a weaker notion of consistency for a geographically distributed database [L7]. We reduced the timing guarantees provided by Spanner's TrueTime protocol to causal dependencies that are specified in a formal calculus.

We described an iterative approach based on formal concept analysis to refine the information retrieval process [L8]. We used a Galois connection to introduce a new type of formal concept that allows us to work with specific thresholds for searching words in Web documents. We use techniques for processing large data sets in parallel, to generate sequences of Galois lattices, overcoming the time complexity of building a lattice for an entire large context.

We presented a topological approach of the web classification, aiming to describe classifications and search processes over the web [L9]. An original feature is provided by the distinctness operators which are able to detect when a document is not in a certain classification class. We proved that there is a bijection between regular distinctness operators and regular topologies. Adding some properties to a regular distinctness operator, we associated it to a regular Alexandrov topology.

We introduced a stochastic process calculus named PHASE which operates with phase-type distributions, and provided a step-by-step description of how PHASE processes can be translated into models supported by the probabilistic model checker PRISM [L10]. We then illustrated our approach by analysing the behaviour of a simple system involving both non-Markovian and Markovian transitions. Furthermore, we provided a case study involving a non-Markovian interactive system, as a means of highlighting the advantages of phase-type approximations, in comparison to approximating non-Markovian transitions through single Markovian transitions [L14,TR1].

We considered present mobile membranes in which the movement is provided by rules inspired by cells endocytosis and exocytosis [L13]. We compared their computational power to the classical notion of Turing computability. These mobile membranes can algorithmically solve hard problems in polynomial time. Finally we compared these multiset rewriting systems with other formalisms as mobile ambients and brane calculi.

Also, the edited volume [VE1] contains the papers of a rank B conference in the organisation of which we were involved.