Research Theme:Concurrency and Distributed Systems (Bradfield, Esparza, Gilmore, Hillston, Stevens, Stirling)

This group works by making foundational innovations, applying them to real-world problems, sometimes in collaboration with industry, and disseminating the techniques in software tools that have large international user communities. The disseminated techniques have strongly influenced the direction of research in this area internationally. Foundational achievements include: solutions to decision problems in classical automata theory (DPDA equivalence) and in infinite state systems; resolution of long-standing expressiveness questions in logics for concurrency (proof of the strict alternation depth hierarchy for modal mu-calculus); the introduction of tableaux techniques for decision problems in concurrency; the use of automata for deciding model checking problems over infinite state systems, and net unfolding techniques to avoid state explosion in the verification of Petri nets; the use of games in the theory of concurrency; and the development of stochastic process algebras providing a compositional approach to performance modelling. Application areas include: safety-critical systems; performance in active networks; protocols for distributed systems. Tools include: PEP (a Petri net tool); the Model Checking Kit; the Edinburgh Concurrency Workbench; and the PEPA Workbench. Bradfield holds an EPSRC Advanced Research Fellowship to study modal mu-calculi, causality, and true concurrency.

Projects

• Verification of Concurrent Systems