An important class of distributed algorithms consists of computer communication protocols. We have worked with the problems of protocol analysis since 1984. We begun by constructing a reachability analysis tool PROTAN88 designed for protocols specified with an extended state transition model (ESTELLE specification language). In the 1980's this tool has been tried out by us in analyzing several well-known real-life protocols like X.25, FTAM and X.411/P1. Some of our improvement suggestions were included in the FTAM state tables published by CCITT and ISO.
Lately, our work has been more conceptual and theoretical. Various equivalence concepts have been studied in process algebra contexts (Milners CCS and ISO LOTOS) and the equivalence preserving minimization of labeled state transition systems has been studied. We have been especially interested in divergence preserving behavioural equivalences and preorders.
The analysis of liveness properties is especially important in the context of specification and verification of temporal logic properties of concurrent systems. Temporal logics are a class of logic-based formal languages containing temporal operators, such as 'sometime' or 'always'. Their applications to verification of concurrent systems have been internationally one of the main research directions in the concurrency research for the last twenty years. In our work on temporal logic, we have examined the preservation of temporal logic properties in the construction of reduced models based on divergence-sensitive equivalences and preorders. We have also examined the relations of temporal logics, particularly the so-called mu-calculi or fixed-point temporal logics, with automata on infinite objects.
A recurrent theme in our research is to make analysis and verification feasible for concurrent systems of realistic size. That is why a goal in our research is to understand and support compositional (or modular) specification and verification of concurrent systems. We have been e.g. analyzing and applying the weakest equivalence (CFFD-equivalence) preserving deadlocks and linear next-timeless linear temporal formulae. Our research employs case analyses (often computer communication protocols) to ensure the practical usefulness of the theoretical concepts.
At the university of Helsinki we have developed a computer-based verification tool BIDMIN allowing us to minimize labeled transition systems with respect to divergence preserving bisimilarity and branching bisimilarity as well as the related congruences. Vesa Hellgren has been developing parallel verification algorithms. The algorithms have been implemented in PAVEL (Parallel Verification of LOTOS/LTS) which is a software running in the Cray T3E supercomputer and a network of Linux workstations. We also often use a LOTOS oriented verification tool ARA TOOLS developed at the Technical Research Centre of Finland.
Current members of the MOCO group are Prof. Martti Tienari (group leader), Doc. Roope Kaivola, M.Sc. Vesa Hellgren, Ph.Lic. Timo Karvi, M.Sc. Päivi Kuuppelomäki and M.Sc. Matti Luukkainen (Nokia Research Centre ). As an associate member of the group we have Prof. Antti Valmari (Tampere University of Technology, Software Systems Laboratory ) who is the chief designer of ARA TOOLS. Our concurrency group has been participating (1994-97) in the European COST247-project Verification and Validation Methods for Formal Descriptions.
Publications: [18, 98, 100, 103, 106-111]. Home Page: http://www.cs.helsinki.fi/research/moco/