Formal Methods Laboratory

We provided a nominal semantics of the monadic version of the fusion calculus [L1]. We presented a set of compact transition rules in the Fraenkel-Mostowski framework by using a specific nominal quantifier. By using several nominal techniques, we proved the equivalence between the new nominal semantics and the original semantics of the monadic fusion calculus.

We verified certain properties of membrane systems through the use of specific techniques and a software tool developed for coloured Petri nets [L2]. We characterised some subclasses of membrane systems in which various qualitative properties (reachability, liveness) and quantitative properties (boundedness) are decidable. We established a formal connection between two multiset rewriting systems (membrane systems with delays and Petri nets with delays), and proved an operational correspondence between them. For both Petri nets and membrane systems we proved that adding finite delays does not increase their expressive power; however, both formalisms become more flexible in describing molecular phenomena where time represents a critical resource.

We introduced a process algebra (PerTiMo) with processes able to migrate between different explicit locations and in which two processes may communicate if they are present at the same location and, in addition, they have appropriate access permissions to communicate over a shared channel [L3]. Access permissions can be acquired or lost while moving from one location to another. We completely characterized the situations in which a process is guaranteed to possess safe access permissions in all possible environments. In this way, one can design and model systems in which processes are not blocked (deadlocked) due to the lack of dynamically changing access permissions.

We developed a new semantic model for the Timed Mobility (TiMo) process algebra using Rewriting Logic (RL) and strategies, with the aim of providing a foundation for tool support; in particular, strategies are used to capture the locally maximal concurrent step of a TiMo specification which previously required the use of action rules based on negative premises [L4]. We extended this RL model with access permissions in order to develop a new semantic model for PerTiMo. We formally proved that these RL semantical models are sound and complete with respect to the original operational semantics on which they were based. We presented examples of how the developed RL models for TiMo and PerTiMo can be implemented within the strategy-based rewriting system Elan and illustrated the range of (behavioural) properties that can be analysed using such a tool.

We introduced new types of similarity relations between objects or attributes in fuzzy attribute-oriented concept lattices [L5]. We analyzed how these similarities are related using the definitions and considering the reducibility between antitone and isotone fuzzy concept lattices as well. A comparison is made between two relations which measures the similarity of fuzzy oriented concepts. These relations are employed in factorizing the fuzzy attribute-oriented concept lattice, in order to reduce its complexity.

We provided an introduction to the Web of Linked Data from the perspective of a Web developer who would like to build an application using Linked Data [L6]. We identified a weakness in the development stack, namely a lack of domain specific scripting languages for designing background processes that consume Linked Data. To address this weakness, we designed a scripting language with a simple but appropriate type system. We proved that our type system is algorithmic; and can therefore be used for minimal type inference. We also proved subject reduction and type safety results, which justify our claim that our language is statically type checked and does not throw basic runtime type errors. We related our work to the W3C recommendations that drive Linked Data, so that our syntax is accessible to Web developers.

We developed a theory of abstract interpretations which is consistent to the principles of constructing the Finitely Supported Mathematics [L7]. We translated the notions of lattices and Galois connections into the framework of invariant sets, and presented their properties in terms of finitely supported objects. We introduced the notions of invariant correctness relation and invariant representation function, we emphasized an equivalence between them, and we established the relationship between these notions and invariant Galois connections. We provide some widening and narrowing techniques in order to approximate the least fixed points of finitely supported transition functions.

We defined finitely supported mathematics by using sets with atoms [L8] Such a mathematics generalizes the classical Zermelo-Fraenkel mathematics, and represents an appropriate framework to work with (infinite) structures in terms of finitely supported objects. We focused on the techniques of translating the Zermelo-Fraenkel results to this finitely supported mathematics over sets with atoms.

In order to illustrate the features of TiMo, we describe a railway control system [L9]. We define some behavioural equivalences matching multisets of actions that could happen in a given range of time (up to a timeout). We also defined the strong time-bounded bisimulation and the strong open time-bounded bisimulation, and proved that the latter one is a congruence. By using various bisimulations over the behaviours of real-time systems, we can check which behaviours are closer to an optimal and safe behaviour.

We extended TiMo by expressing the time constraints as bounded intervals in order to model the uncertainty of the delay in migration and communication of agents placed in the locations of a distributed system [L10]. We provided the operational semantics, and illustrated the new language by a detailed example for which we used software tools for analyzing its temporal properties.

We looked at the living cells as complex systems of ion pumps working in parallel to ensure proper physiologic functionalities [L11]. To model such a system of pumps, we defined a formalism called BioMaxP that allows working with multisets of ions, explicit interpretation of the transportation (from inside to outside, and from outside to inside) based on the number of existing ions, and a maximal parallel execution of the involved pumps.

We introduced the notion of descriptive typing that assigned to resources in Linked Data provide useful annotations that describe how a resource may be used [L13]. Instead of raising compile time errors, a descriptive type system raises runtime warnings with a menu of options that make suggestions to the programmer. We introduced a subtype system, algorithmic type system and operational semantics that work together to characterise how descriptive types are used. The type system enables RDF Schema inference and several other modes of inference that are new to Linked Data.

We defined a formalism inspired by cell biology in which mobility and timing are explicitly specified [L14]. In order to reason about the behaviours of complex biological systems, we introduced several observational equivalences over mobile membranes with lifetimes. These equivalences correspond to several combinations of mobility operations that can be performed, timing aspects of the objects involved in mobility and their explicit positions inside membranes. We proved various relationships between these observational equivalences and used the ambient logic to provide a logical characterization for located observational equivalence.

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 [L15]. We used a simple version of distributed pi-calculus to define mobility types. The novelty of this approach is that we point out sequences of migrations as global types, and investigate 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 [L16]. 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 .

We introduced and studied a process algebra called TiMo [L12]. A probabilistic extension of TiMo assigns probabilities to the transitions that describe the behaviour of TiMo networks by solving the nondeterminism involved in the movement and in the communication of processes, as well as in the selection of active locations [L17]. We defined a novel logic called PLTM (Probabilistic Logic for Timed Mobility) that is able to describe certain aspects that are not commonly found in other logics, such as the ability to check properties which make explicit reference to specific locations and processes, to impose temporal constraints over local clocks (finite or infinite upper bounds, for each location independently), to define complex action guards over multisets of actions and properties for transient and steady-state behaviours. We presented a verification algorithm for PLTM, and determined its time complexity. Given that PLTM operates at the level of discrete-time Markov chains, it can also be applied to other process algebras which involve locations, timers, process movements and communications.