Informace o projektu
Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů
- Kód projektu
- MSM 143300001
- Období řešení
- 1/1999 - 12/2004
- Investor / Programový rámec / typ projektu
-
Ministerstvo školství, mládeže a tělovýchovy ČR
- Výzkumné záměry
- Fakulta / Pracoviště MU
- Fakulta informatiky
- Klíčová slova
- concurrency;process algebras; infinite state systems; real-time; modal and temporal logics;concurrent constraint systems;specification;verification;quantum algorithms and protocols;entanglement;quantum finite and cellular automata;design methodologies
Cíl: Význam nesekvenčních modelů výpočetních procesů vzrůstá jak z hlediska teoretického, tak praktického. Cílem tohoto návrhu pro dlouhodobý výzkumný záměr je jak pokračování v již existujícím úspěšném výzkumu v oblasti souběžných (concurrent) distribuovaných systémů, tak i rozšíření výzkumu na problematiku kvantových modelů a výpočtů. Obsah: Analýza modelů souběžných procesů a jejich vzájemných vztahů s důrazem na algoritmické a složitostní aspekty. Analýza modelů a návrh specifikačních a transformačních nástrojů pro souběžné systémy pracující v reálném čase s důrazem na tzv. safety-critical systémy. Logiky, zejména temporální a modální, pro specifikaci a analýzu souběžných systémů. Návrh a analýza kvantových algoritmů a vývoj metod pro návrh kvantových algoritmů a protokolů, jakož i kvantových konečných automatů a celulárních automatů.
Výsledky
Cílem tohoto návrhu pro dlouhodobý výzkumný záměr je jak pokračování v již existujícím úspěšném výzkumu v oblasti souběžných (concurrent) distribuovaných systémů, tak i rozšíření výzkumu na problematiku kvantových modelů a výpočtů.
Publikace
Počet publikací: 264
2007
-
Height-Deterministic Pushdown Automata
32nd International Symposium on Mathematical Foundations of Computer Science (MFCS'07), rok: 2007
2006
-
Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols
Automated Technology for Verification and Analysis (ATVA'06), rok: 2006
-
Undecidability Results for Bisimilarity on Prefix Rewrite Systems
LNCS, Foundations of Software Science and Computation Structures (FOSSACS'06), rok: 2006, ročník: 2006, vydání: 3921
-
Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation
LNCS, Annual Conference on Computer Science Logic (CSL'06), rok: 2006, ročník: 2006, vydání: 4207
2005
-
On Counting the Number of Consistent Genotype Assignments for Pedigrees
Proceedings of 25th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'05), rok: 2005
2004
-
A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications
Proceedings of 15th International Conference on Concurrency Theory (CONCUR 2004), rok: 2004
-
A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata
Exploring New Frontiers of Theoretical Informatics : IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004), rok: 2004
-
Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.
Formal Methods in Computer-Aided Design (FMCAD), rok: 2004
-
Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.
Rok: 2004, počet stran: 22 s.
-
Completeness Results for Undecidable Bisimilarity Problems
Proccedings of the 5th International Workshop on Verification of Infinite-State Systems (INFINITY'03), rok: 2004