appearance

MU › Research and development › List of projects › Project details › Research Project Results

Skip navigation

Skip the Organizational structure panel
Organizational structure
On selecting a constituent part of MU the "Overview of publishing activities" page will be displayed with information relevant to the selected constituent part. The "Overview of publishing activities" 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
- International Studies
- Disabled Students
- Technology Transfer
- Biostatistics
- Mendel Museum
- CERIT
- Civic Education

Masaryk University

Research Project Results

<< back

Infinite state concurrent systems - models and verification

Project Identification:

GA201/00/0400

MU Investigator:

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

MU Faculty/Unit:

Faculty of Informatics

Project Period:

1/2000 - 12/2002

Investor/Programme:

Czech Science Foundation / Standard Projects-

Cooperating Organization:

Technical University Ostrava

Publications:

2004

DP lower bounds for equivalence-checking and model-checking of one-counter automata

JANČAR, Petr - KUČERA, Antonín - MOLLER, Faron - SAWA, Zdeněk.
DP lower bounds for equivalence-checking and model-checking of one-counter automata. Information and Computation, , Academic Press, USA. ISSN 0890-5401, 2004, vol. 188, no. 1, pp. 1-19.

2003

Coordination by means of Synchronous and Asynchronous Communication in Concurrent constraint Programming

BRIM, Luboš - JACQUET, Jean-Marie - GILBERT, David - KŘETÍNSKÝ, Mojmír.
Coordination by means of Synchronous and Asynchronous Communication in Concurrent constraint Programming. Electronic Notes in Theoretical Computer Science, Amsterdam, Elsevier Science. ISSN 0444514163, 2003, vol. 68, no. 3, pp. 1-24.

2002

Boundaries and Efficiency of Verification

STREJČEK, Jan.
Boundaries and Efficiency of Verification. In Proceedings of summer school MOVEP~2002. Nantes (France) : IRCCyN, Ecole Centrale de Nantes, France, 2002. pp. 403-408. 2002, 17.-21. 6. 2002, Nantes (France).

CONCUR 2002 - Concurrency Theory. 13th International Conference.

BRIM, Luboš - JANČAR, Petr - KŘETÍNSKÝ, Mojmír - KUČERA, Antonín.
CONCUR 2002 - Concurrency Theory. 13th International Conference. 2002. Czech Republic, Brno. 20.8.2002 - 23.8.2002, Worldwide Activity.

CONCUR 2002 - Concurrency Theory. 13th International Conference. Proceedings.

BRIM, Luboš - JANČAR, Petr - KŘETÍNSKÝ, Mojmír - KUČERA, Antonín.
CONCUR 2002 - Concurrency Theory. 13th International Conference. Proceedings. Berlin, Heidelberg, New York : Springer, 2002. 609 s. Lecture Notes in Computer Science, vol. 2421. ISBN 3-540-44043-7.

Coordination by means of Synchronous and Asynchronous Communication in Concurrent constraint Programming

BRIM, Luboš - JACQUET, Jean-Marie - GILBERT, David - KŘETÍNSKÝ, Mojmír.
Coordination by means of Synchronous and Asynchronous Communication in Concurrent constraint Programming. In Foundations of Coordination Languages and Software Architecture (FOCLASA`02). Amsterdam : Namur University, 2002. pp. 1-24. 2002, August 2002, Brno.

Equivalence-Checking with Infinite-State Systems: Techniques and Results.

KUČERA, Antonín - JANČAR, Petr.
Equivalence-Checking with Infinite-State Systems: Techniques and Results. In Proceedings of 29th Conference on Current Trends in Theory and Practice of Informatics (SOFSEM 2002). Berlin : Springer, 2002. ISBN 3-540-00145-X, pp. 41-73. 2002, November 22-29, 2002, Milovy, Czech Republic.

Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds

JANČAR, Petr - KUČERA, Antonín - MOLLER, Faron - SAWA, Zdeněk.
Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds. In Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002). Berlin, Heidelberg, New York : Springer, 2002. ISBN 3-540-43366-X, pp. 172-186. 2002, Grenoble, France, April 8-12, 2002.

Infinity 2002. 4th International Workshop on Verification of Infinite-State Systems

KUČERA, Antonín - MAYR, Richard.
Infinity 2002. 4th International Workshop on Verification of Infinite-State Systems. Amsterdam : Elsevier, 2002. 106 s. ENTCS, volume 68(6). ISBN 0444513299.

Modifications of Expansion Trees for Weak Bisimulation in BPA

ČERNÁ, Ivana - STŘÍBRNÁ, Jitka.
Modifications of Expansion Trees for Weak Bisimulation in BPA. In Verification of Infinite-State Systems Infinity'2002. The Netherlands : Elsevier Science Publishers, 2002. ISBN 0444512918, pp. 1-21. 2002, 24.8.2002, Brno, Czech Republic.

Note on the Tableau Technique for Commutative Transition Systems

SRBA, Jiří.
Note on the Tableau Technique for Commutative Transition Systems. In Proceedings of 5th Foundations of Software Science and Computation Structures (FOSSACS'02). Holland : Springer-Verlag, 2002. pp. 387-401. 2002, 6-14. 4 2002, Grenoble, France.

On the Complexity of Semantic Equivalences for Pushdown Automata and BPA

KUČERA, Antonín - MAYR, Richard.
On the Complexity of Semantic Equivalences for Pushdown Automata and BPA. In Proceedings of 27th International Symposium on Mathematical Foundations of Computer Science (MFCS 2002). Berlin : Springer, 2002. ISBN 3-540-44040-2, pp. 433-445. 2002, August 26-30, 2002, Warsaw, Poland.

Roadmap of Infinite Results

SRBA, Jiří.
Roadmap of Infinite Results. Bulletin of the European Association for Theoretical Computer Science, Bratislava, EATCS, Slovakia. ISSN 78, 2002, vol. 2002, no. 78, pp. 163-175.

Simulation Preorder over Simple Process Algebras

KUČERA, Antonín - MAYR, Richard.
Simulation Preorder over Simple Process Algebras. Information and Computation, , Academic Press, USA. ISSN 0890-5401, 2002, vol. 173, no. 2, pp. 184-198.

SRBA, Jiří.
Strong Bisimilarity and Regularity of Basic Parallel Processes is PSPACE-Hard. In Proceedings of 19th International Symposium on Theoretical Aspects of Computer Science (STACS'02). Holland : Springer-Verlag, 2002. pp. 535-546. 2002, 14-16 March, 2002, Juan les Pins, France.

SRBA, Jiří.
Strong Bisimilarity and Regularity of Basic Process Algebra is PSPACE-Hard. In Proceedings of 29th International Colloquium on Automata, Languages and Programming (ICALP'02). Netherlands : Springer-Verlag, 2002. pp. 716-727. 2002, July 2002, Malaga, France.

The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL

KUČERA, Antonín - STREJČEK, Jan.
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'02). Berlin : Springer, 2002. ISBN 3-540-44240-5, pp. 276-291. 2002, September 22-25, 2002, Edinburgh, Scotland.

Undecidability of Weak Bisimilarity for Pushdown Processes

SRBA, Jiří.
Undecidability of Weak Bisimilarity for Pushdown Processes. In Proceedings of 13th International Conference on Concurrency Theory (CONCUR'02). Holland : Springer-Verlag, 2002. pp. 579-593. 2002, August 2002, Brno, Czech Republic.

KUČERA, Antonín - MAYR, Richard.
Weak Bisimilarity between Finite-State Systems and BPA or normed BPP is Decidable in Polynomial Time. Theoretical Computer Science, Amsterdam, Nizozemí, , The Nederlands. ISSN 0304-3975, 2002, vol. 270, no. 1-2, pp. 677-700.

Why is Simulation Harder Than Bisimulation?

KUČERA, Antonín - MAYR, Richard.
Why is Simulation Harder Than Bisimulation?. In Proceedings of 13th International Conference on Concurrency Theory (CONCUR 2002). Berlin : Springer, 2002. ISBN 3-540-44043-7, pp. 594-609. 2002, August 20-23, 2002, Brno, Czech Republic.

2001

Basic Process Algebra with Deadlocking States

SRBA, Jiří.
Basic Process Algebra with Deadlocking States. Theoretical Computer Science, , , The Nederlands. ISSN 0304-3975, 2001, vol. 2001, no. 266(1-2), pp. 605-1234.

Distributed LTL Model-Checking Based on Negative Cycle Detection

BRIM, Luboš - ČERNÁ, Ivana - KRČÁL, Pavel - PELÁNEK, Radek.
Distributed LTL Model-Checking Based on Negative Cycle Detection. In FST-TCS 2001. Bangalore, India : Springer, 2001. ISBN 3-540-43002-4, pp. 96-110. Bangalore, India.

Multi-Agents Systems as Concurrent Constraint Processes

BRIM, Luboš - JACQUET, Jean-Marie - GILBERT, David - KŘETÍNSKÝ, Mojmír.
Multi-Agents Systems as Concurrent Constraint Processes. In SOFSEM 2001 28th Conf.on Current Trends in Theory and Practice of Informatics. Heldelberg : Springer Verlag, 2001. ISBN 0302-9743, pp. 201-210. November 2001, Piestany.

On the Power of Labels in Transition Systems

SRBA, Jiří.
On the Power of Labels in Transition Systems. In Proceedings of 12th International Conference on Concurrency Theory (CONCUR'01). Holland : Springer-Verlag, 2001. pp. 277-567. August 21-24 2001, Aaborg, Denmark.

Properties of Distributed Timed-Arc Petri Nets

NIELSEN, Mogens - SASSONE, Vladimiro - SRBA, Jiří.
Properties of Distributed Timed-Arc Petri Nets. In Proceedings of 21st International Conference on Foundations of SoftwareTechnology and Theoretical Computer Science (FSTTCS'01). Holland : Springer Verlag, 2001. pp. 280-291. 14-16.12. 2001, Bangalore, India.

Randomization Helps in LTL Model Checking

BRIM, Luboš - ČERNÁ, Ivana - NEČESAL, Martin.
Randomization Helps in LTL Model Checking. In Process Algebra and Probabilistic Methods. Proceedings of PAPM-PROBMIV 2001. Berlin Heidelberg New York : Springer, 2001. ISBN 3-540-42556-X, pp. 105-119. Aachen, Germany, September 12-14, 2001.

Rewrite Systems with Constraints

STREJČEK, Jan.
Rewrite Systems with Constraints. In EXPRESS'01 the 8th International Workshop on Expressiveness in Concurrency. Aalborg (Denmark) : Elsevier Science, 2001. pp. 1-20. 20. 8. 2001, Aalborg, Denmark.

Towards a Notion of Distributed Time for Petri Nets

NIELSEN, Mogens - VLADIMIRO, Sassone - SRBA, Jiří.
Towards a Notion of Distributed Time for Petri Nets. In Proceedings of 22nd International Conference on Application and Theory ofPetri Nets (ICATPN'01). Holland : Springer-Verlag, 2001. pp. 23-53. June 25-29 2001, Newcastle, UK.

2000

Complexity of Weak Bisimilarity and Regularity for BPA and BPP

SRBA, Jiří.
Complexity of Weak Bisimilarity and Regularity for BPA and BPP. In Expressiveness in Concurrency, EXPRESS'00. Vyd. 1. State College : Elsevier, 2000. pp. 1-20. August 2000, State College (Penn., USA).

Constrained Rewrite Transition Systems

STREJČEK, Jan.
Constrained Rewrite Transition Systems. Brno : FI MU, 2000. Report Series, FIMU-RS-2000-12. link to a new window WWW.

Efficient Verification Algorithms for One-Counter Processes

KUČERA, Antonín.
Efficient Verification Algorithms for One-Counter Processes. In Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP 2000). Berlin, Heidelberg, New York : Springer, 2000. ISBN 3-540-67715-1, pp. 317-328. July 2000, Geneva, Switzerland.

JOMP Application Program Interface

BULL, Mark - OBDRŽÁLEK, Jan.
JOMP Application Program Interface. Vyd. Version 0.1 (draft). Edinburgh : EPCC Technical Report, 2000. 32 s.

Matching Modulo Associativity and Idempotency is NP-Complete

KLÍMA, Ondřej - SRBA, Jiří.
Matching Modulo Associativity and Idempotency is NP-Complete. In Mathematical Foundation of Computer Science 2000, 25th International Symposium. Berlin : Springer-Verlag, 2000. ISBN 3-540-67901-4, pp. 456-466. 24.-30.9.2000, Bratislava, SK.

OpenMP for Java

OBDRŽÁLEK, Jan.
OpenMP for Java. University of Edinburgh : EPCC Technical Report, 2000. 25 s.

Simulation and Bisimulation over One-Counter Processes

JANČAR, Petr - KUČERA, Antonín - MOLLER, Faron.
Simulation and Bisimulation over One-Counter Processes. In Proceedings of 17th Annual Symposium on Theoretical Aspects of Computer Science (STACS 2000). Berlin, Heidelberg, New York : Springer, 2000. ISBN 3-540-67141-2, pp. 334-345. February 2000, Lille, France.

Some Remarks on Weak Bisimilarity of BPA-Processes

ČERNÁ, Ivana - STŘÍBRNÁ, Jitka.
Some Remarks on Weak Bisimilarity of BPA-Processes. Brno : FI MU Brno, 2000. 26 s. FIMU-RS-2000-09.

Towards OpenMP for Java

BULL, Mark - KAMBITES, Mark - OBDRŽÁLEK, Jan - WESTHEAD, Martin.
Towards OpenMP for Java. In Proceedings of the Second European Workshop on OpenMP (EWOMP 2000). Edinburgh : University of Edinburgh, 2000. pp. 98-105. 2000, University of Edinburgh.

top