As a byproduct of our first goal, we will enrich the theory of ordered sets with themes that are close to application in computer science; in the reverse direction, we will get profit of the theoretic knowledge to improve our understanding of the applicative domain. In particular, a better knowledge of the heuristics implemented in verification tools will allow us to study their computational complexity, to improve them, and to obtain better verification tools.
A second goal of the project -- of an applied nature -- is to develop and improve verification tools for parallel, distributed, and concurrent systems.
We shall focus on two subjects of the theory of ordered sets that are more appealing for the applications to parallel, distributed, and concurrent computation.
The first theme -- which we locate within the more general theme of the semantics of concurrency -- is the specification of infinite ordered sets by means of finite methods. Its investigation will recur to the theory of traces and of automata with independence relations. The notion of circular order will be investigated as well. Mastering this theme will allow us to understand the fine structure of the semantics of concurrency, which is traditionally defined by means of ordered structures.
The second theme is the combinatorics and algebra of finite ordered sets. We shall investigate the combinatorics of traces that model concurrent executions and the algebra of dynamic systems whose order relation on reachable states is a lattice. We recall that a fundamental problem for implementing verification tools is the explosion of the number of states of the systems to be verified: mastering the combinatorics of ordered sets will allow us to develop feasible algorithms to explore states of concurrent systems.
Our work will be completed by the development of two tools whose goal is to specify and verify concurrent systems, AMSC and ELSE. These tools specifically rely on the representation of concurrent executions by means of ordered sets. The first tool allows the analysis of message sequence charts that are used to specify protocols. The second will allow the feasible exploration of the set of states of a concurrent system.