Informace o projektu
Nekonečně stavové souběžné systémy - modely a verifikace

Informace

Projekt nespadá pod Fakultu sportovních studií, ale pod Fakultu informatiky. Oficiální stránka projektu je na webu muni.cz.

Kód projektu

GA201/00/0400

Období řešení

1/2000 - 12/2002

Investor / Programový rámec / typ projektu

Grantová agentura ČR

Standardní projekty

Fakulta / Pracoviště MU

Fakulta informatiky

prof. RNDr. Mojmír Křetínský, CSc.

WWW stránky projektu

http://www.fi.muni.cz/usr/kretinsky/projects/GACR201000400.html

Spolupracující organizace

Vysoká škola báňská - Technická univerzita v Ostravě

Odpovědná osoba prof. RNDr. Petr Jančar, CSc.

Projekt je motivován jednou z živých oblastí současného výzkumu týkajícího se modelování, analýzy a verifikace složitých (potenciálně nekonečně stavových) souběžných (concurrent) systémů. Jejich verifikací se rozumí (zkoumání možností algoritmického) ověřování jistých ekvivalencí těchto systémů, jejich temporálně logických vlastností apod. V poslední době bylo v dané oblasti dosaženo zajímavých výsledků, např. pro kalkuly BBA, BPP, PA a Petriho sítě, k nimž přispěly grant. projekty GAČR č. 201/93/2123 a č. 210/97/0456 řešené týmem, který předkládá tento návrh. Hlavním cílem navrhovaného projektu je systematicky prozkoumat zmíněné a příbuzné modely a zaměřit se na charakterizaci rozhodnutelných podtříd vzhledem k běžným ekvivalencím a jejich vzájemné vztahy, testování regularity (tj. ekvivalence s konečně stavovým systémem) a možností konečné charakterizace (i vzhledem k adekvátním předuspořádáním), a na rozhodnutelné modální a temporální logiky, či rozumné fragmenty.

Publikace

Počet publikací: 36

2001

Distributed LTL Model-Checking Based on Negative Cycle Detection

BRIM Luboš ČERNÁ Ivana KRČÁL Pavel PELÁNEK Radek

Článek ve sborníku

FST-TCS 2001, rok: 2001
Multi-Agents Systems as Concurrent Constraint Processes

BRIM Luboš JACQUET Jean-Marie GILBERT David KŘETÍNSKÝ Mojmír

Článek ve sborníku

SOFSEM 2001 28th Conf.on Current Trends in Theory and Practice of Informatics, rok: 2001
On the Power of Labels in Transition Systems

SRBA Jiří

Článek ve sborníku

Proceedings of 12th International Conference on Concurrency Theory (CONCUR'01), rok: 2001
Properties of Distributed Timed-Arc Petri Nets

NIELSEN Mogens SASSONE Vladimiro SRBA Jiří

Článek ve sborníku

Proceedings of 21st International Conference on Foundations of SoftwareTechnology and Theoretical Computer Science (FSTTCS'01), rok: 2001
Randomization Helps in LTL Model Checking

BRIM Luboš ČERNÁ Ivana NEČESAL Martin

Článek ve sborníku

Process Algebra and Probabilistic Methods. Proceedings of PAPM-PROBMIV 2001, rok: 2001
Rewrite Systems with Constraints

STREJČEK Jan

Článek ve sborníku

EXPRESS'01 the 8th International Workshop on Expressiveness in Concurrency, rok: 2001
Towards a Notion of Distributed Time for Petri Nets

NIELSEN Mogens VLADIMIRO Sassone SRBA Jiří

Článek ve sborníku

Proceedings of 22nd International Conference on Application and Theory ofPetri Nets (ICATPN'01), rok: 2001

2000

Complexity of Weak Bisimilarity and Regularity for BPA and BPP

SRBA Jiří

Článek ve sborníku

Expressiveness in Concurrency, EXPRESS'00, rok: 2000
Constrained Rewrite Transition Systems

STREJČEK Jan

Prezentace v oblasti VaV (AV tvorba, WEB aplikace apod.)

Rok: 2000, druh: Prezentace v oblasti VaV (AV tvorba, WEB aplikace apod.)
Efficient Verification Algorithms for One-Counter Processes

KUČERA Antonín

Článek ve sborníku

Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP 2000), rok: 2000