Faculty of Informatics logo Infinite-State Concurrent Systems - Models and Verification
- - - - -
Funding: Grant Agency of Czech Republic, Project No. 201/00/0400
Starting Date: January 1, 2000
Duration: 3 years
Project Leader: M. Kretinsky
Co-leader: P. Jancar (TU Ostrava)
- - - - -

This project is motivated by one of the current research trends in concurrency theory, i.e. by modelling, analysis and verification of concurrent infinite state systems. Verification is understood as (an examination of possibly algorithmic) checking of semantic equivalences between these systems (processes) or checking their properties expressed in suitable modal logics etc.

Recently, some interesting results have been achieved in this area, e.g. for calculi BPA, PDA, BPP, PA and Petri nets; some contributions were made by members of this project research team (see past projects of of the Grant Agency of the Czech Republic, grant no. 201/93/2123 and grant no. 201/97/0456 ).

The main goal is to investigate the mentioned and related classes with aims

  • to characterise (sub)classes w.r.t. decidability of (some) semantic (behavioral) equivalences,
  • to describe their relationships,
  • to study regularity conditions, and
  • to examine the possibilities of their so called characterisations w.r.t. relevant preorders.
Also it is suggested to study decidability issues of modal and temporal logics (or their reasonable fragments) for these classes. The other goal is to investigate models for concurrent constrained processes which allows synchronous communication as well, and to develop frameworks for reasoning about these systems.
- - - - -
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)
Z. Sawa (TU Ostrava)
- - - - -
Contact M. Kretinsky
- - - - -
Publications List of publications, year 2000
- - - - -
Associated GACR Post-Doc projects running at FI MU :