Go to main content | Go to main menu | Go to search

Project information
Verification of infinite-state systems

Investor logo
Project Identification
GA201/03/1161
Project Period
1/2003 - 12/2005
Investor / Pogramme / Project type
Czech Science Foundation
  • Standard Projects
MU Faculty or unit
Faculty of Informatics
Keywords
concurrency theory, infinite-state systems, equivalence checking, decidability, complexity
Cooperating Organization
Technical University Ostrava
  • Responsible person prof. RNDr. Petr Jančar, CSc.

This project proposal 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 the team submitting
this proposal.


The main goal is to investigate the mentioned and related classes with
aims to characterise (sub)classes w.r.t.~decidability of (some)
equivalences and preorders, to describe their mutual relationship and
relative expressibility (incl.\,regularity and so called
characterisations w.r.t.\,preorders), and to study complexity of
respective decision algorithms. Also it is suggested to study
decidability and complexity issues of modal and temporal logics (or
their fragments) for these classes. The other goal is to investigate
(not only monotonic) models for concurrent constrained processes to
allow asynchronous and synchronous communication, and to develop
frameworks for reasoning about these systems.

Publications

Total number of publications: 43

2005

2004

Previous 1 2 3 4 5 Next

You are running an old browser version. We recommend updating your browser to its latest version.

More info