Model Checking Large Finite-State Systems and Beyond

BRIM, Luboš and Mojmír KŘETÍNSKÝ. Model Checking Large Finite-State Systems and Beyond. In 33rd Conference on Current Trends in Theory and Practice of Computer Science. Berlin: Springer-Verlag, 2007, p. 9-28. ISBN 978-3-540-69506-6.

Basic information

Original name

Model Checking Large Finite-State Systems and Beyond

Name in Czech

Ověřování modelu pro rozsáhlé konečně stavové systémy a za jejich hranicemi

Authors

BRIM, Luboš (203 Czech Republic, guarantor) and Mojmír KŘETÍNSKÝ (203 Czech Republic)

Edition

Berlin, 33rd Conference on Current Trends in Theory and Practice of Computer Science, p. 9-28, 20 pp. 2007

Publisher

Springer-Verlag

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/07:00019356

Organization unit

Faculty of Informatics

ISBN

978-3-540-69506-6

UT WoS

000244537600002

Keywords in English

finite and infinite-state systems; reachability; linear time logic; model checking; decidability

Tags

decidability, finite and infinite-state systems, linear time logic, Model checking, reachability

Tags

International impact, Reviewed

---

Abstract

V originále

We establish a decidability boundary of the model checking problem for infinite-state systems defined by Process Rewrite Systems (PRS), possibly extended with a weak finite-state control unit, and properties described by basic fragments of action-based Linear Temporal Logic (LTL) a Hennessy-Milner branching time logic.

In Czech

Je ustanovena hranice rozhodnutelnosti pro problém ověřování modelu pro fragmenty logik HM resp. LTL a nekonečně stavové systémy generované tzv. procesovými přepisovacími systémy (eventuelně rozšířenými o tzv.slabou 59dic9 jednotku.

---

Links

GA201/06/1338, research and development project	Name: Automatizovaná verifikace softwaru Investor: Czech Science Foundation, Automated software verification
MSM0021622419, plan (intention)	Name: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1ET408050503, research and development project	Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science