Faculty of Informatics logo Algorithmic Verification Boundaries for Infinite-State Systems
- - - - -
Funding: Grant Agency of Czech Republic, Project No. 201/97/0456
Starting Date: January 1, 1997
Duration: 3 years
Coordinator: P. Jancar (TU Ostrava)
Project Leader at FI: M. Kretinsky
- - - - -
Description The project is motivated by a live current research area concerning analysis and verification of complex (infinite-state) concurrent systems. It is the area of boundaries for algorithmic verification, where verification means checking equivalences of systems, their temporal logic properties etc.

Recently, several interesting results have been obtained in the given area, e.g. for calculi BPA, BPP, and Petri nets, to which also the grant of the Grant Agency of the Czech Republic, grant no. 201/93/2123 by the same research team, has contributed.

The main target of the proposed project is to explore systematically the mentioned and related models and focus on

  • characterization of decidable subclasses wrt usual equivalences,
  • testing regularity (i.e. equivalence with a finite-state system),
  • decidable modal and temporal logics, or reasonable fragments.
It is also planned to study complexity of relevant algorithms, and for suitable cases their implementation and testing. In addition, the recent research area of concurrent constraint systems will be explored wrt the mentioned questions.
- - - - -
Cooperating
Organisations		 Faculty of Informatics, Masaryk University Brno
Technical University Ostrava
- - - - -
People L. Brim (FI)
I. Cerna (FI)
P. Jancar (TU Ostrava)
M. Kretinsky (FI)
A. Kucera (FI)
J. Srba (FI)
- - - - -
Contact M. Kretinsky
- - - - -
Publications List of publications (by FI staff only)
- - - - -
Other
Information

MFCS'98 Workshop on Concurrency - Algorithms and Tools

August 27-29, 1998, Brno, Czech Republic

The workshop was organised as a part of the project with focus on the problem of modelling, testing, and verification of concurrent systems. This area has recently attracted a lot of attention - a large theory answering many interesting questions has been developed, and parts of the theory have also been applied. The aim of the workshop was to highlight promising theoretical approaches and paradigms which affect the development of practical tools for (semi)automatic verification of concurrent systems. Working experimental tools were presented.