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

Project information
Verification of infinite-state systems

Information

This project doesn't include Faculty of Medicine. It includes Faculty of Informatics. Official project website can be found on muni.cz.
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

2004

  • Recursive Ping-Pong Protocols

    HUTTEL Hans SRBA Jiří

    Article in Proceedings

    Proceedings of 4th International Workshop on Issues in the Theory of Security (WITS'04), year: 2004

  • Roadmap of Infinite Results

    SRBA Jiří

    Article in Periodical

    Current Trends in Theoretical Computer Science, The Challenge of the New Century, year: 2004, volume: 2, edition: 1

2003

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