• Skip the Organizational structure panel
• Organizational structure

  On selecting a constituent part of MU the "List of projects" page will be displayed with information relevant to the selected constituent part. The "List of projects" page is not available for non-activated items.

  Masaryk University

  • Faculties
  • Law
  • Medicine
  • Science
  • Arts
  • Education
  • Economics
  • Informatics
  • Social Studies
  • Sports Studies

  • Institutes
  • Computer Science
  • Political Science
  • CEITEC
  • Specialized Units
  • Hostels & Canteens
  • University Press
  • Telč Centre
  • UCB Management

  • Rector`s Office
  • Rectorate
  • Other Units
  • Archive
  • Language Centre
  • Mendel Museum
  • Disabled Students
  • International Studies
  • Technology Transfer
  • Biostatistics

   

Project details

Infinite state concurrent systems - models and verification

Project Identification:	GA201/00/0400
Project Period:	1/2000 - 12/2002
Investor:	Czech Science Foundation
Programme / Project Type:	Standard Projects
MU Faculty/Unit:	Faculty of Informatics MU Investigator: Prof. RNDr. Mojmír Křetínský, CSc.
Cooperating Organization:	Technical University Ostrava Responsible Person: Prof. RNDr. Petr Jančar, CSc.
Field:	JC - Computer hardware and software (J - Industry) BA - General mathematics (B - Physics and mathematics)
Publications/Results:	more
Project Website:	http://www.fi.muni.cz/usr/kretinsky/projects/GACR201000400.html

This project proposal is motivated by one of the concurrent research trends in concurrency theory, e.i. by modelling, analysis and verification of concurrent infinite state systems. Verification is understood as (an examination of possibly algorithmic) c hecking 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, to describe their relati onships, 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 a temporal logics (or their reasonable fragments) for the