Research Projects - Specification and Verification of Concurrent Systems
Specification and Verification of Concurrent Systems
The research in the scope of the project "Specification and
Verification of Concurrent Systems" currently focuses on Petri nets,
unfolding techniques, non-interleaving semantics and graph
transformation systems. Our group has a long tradition of research in
this area. For more information visit the pages of our former projects.
In concurrency theory there is a large variety of models. Our main
interest lies on Petri nets, process calculi such as CCS and the
pi-calculus, and graph transformation systems.
Verification and analysis of concurrent systems is especially
challenging since it means taking into account interferences and
conflicts between the subcomponents of a system. Even for
finite-state systems concurrency typically leads to a huge state
space, even for small system descriptions, a phenomenon called state
space explosion. One solution is to employ unfolding techniques in
order to minimize the growth of the state space.
Further problems arise in the verification of infinite-state systems,
although automated techniques exist for restricted classes of models.
One possible solution would be to resort to non-complete but automatic
analysis techniques, which are allowed to answer "don't know" in some
Below the descriptions of some specific research projects are listed.
Multi-agent systems (Astrid Kiehn)
Giving autonomy to the components of a concurrent system one obtains
so-called multiagent systems. The components (now called agents) are
autonomous in their decisions and actions and may have
learning facilities. There is an increasing interest in multiagent
systems as the internet supplies the infrastructure and many
applications for a respective software technology. As it is
open and under permanent change, the agents must be able to cope with
partial, uncertain knowledge and, based on this, adapt their behaviour.
Due to its pragmatic reasoning the belief-desire-intention (BDI) model
has turned out to be a useful abstraction tool for describing,
explaining and predicting the behaviour of agents. We consider
mathematical formalism for specifying and verifying BDI-based systems.
Graph transformation systems (Barbara König)
Graph rewriting can be seen as a general framework in which to specify
and reason about concurrent and distributed systems. The topology and
connection structure of these systems can often be naturally
represented in terms of nodes and connecting edges, and their dynamic
evolution can be expressed by graph rewriting rules. There are several
graph transformation approaches, among them the well-known
double-pushout approach introduced by Ehrig.
We are especially interested in the verification and static analysis
of graph transformation systems. In this context we developed a theory
of bisimulation for graph transformation systems and introduced
analysis techniques, based on type systems and unfoldings respectively.
University of Edinburgh
(Javier Esparza, Julian Bradfield,
Universita di Pisa
Indian Institute of Technology, Delhi
(S. Arun Kumar, Sanjiva Prasad),
Institute at Sophia-Antipolis (Davide
Masaryk University, Brno
Master's Theses, Term Projects
Have a look at the topics which are
currently offered. If you are interested in another topic please
contact us directly.
Links to Related Sites
Formal Models of Concurrency:
Formal Verification in Industry (examples):
Last modified: Tue Aug 27 09:48:21 MET DST 2002