On Refinement of Büchi Automata for Explicit Model Checking

BLAHOUDEK, František, Alexandre DURET-LUTZ, Vojtěch RUJBR and Jan STREJČEK. On Refinement of Büchi Automata for Explicit Model Checking. In Fischer, Bernd and Geldenhuys, Jaco. 2015 International SPIN Symposium on Model Checking of Software. Heidelberg, New York, Dordrecht, London: Springer International Publishing, 2015, p. 66-83. ISBN 978-3-319-23403-8. Available from: https://dx.doi.org/10.1007/978-3-319-23404-5_6.

Basic information

Original name

On Refinement of Büchi Automata for Explicit Model Checking

Name in Czech

O zpřesňování Büchiho automatů pro explicitní metodu ověřování modelu.

Authors

BLAHOUDEK, František (203 Czech Republic, belonging to the institution), Alexandre DURET-LUTZ (250 France), Vojtěch RUJBR (203 Czech Republic, belonging to the institution) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

Heidelberg, New York, Dordrecht, London, 2015 International SPIN Symposium on Model Checking of Software, p. 66-83, 18 pp. 2015

Publisher

Springer International Publishing

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/15:00080986

Organization unit

Faculty of Informatics

ISBN

978-3-319-23403-8

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-23404-5_6

UT WoS

000363788300006

Keywords in English

linear temporal logic; Büchi automata; explicit model checking; specification refinement

Tags

best, Büchi automata, firank_B, formela-conference, LTL, Model checking

Tags

International impact, Reviewed

---

Abstract

V originále

In explicit model checking, systems are typically described in an implicit and compact way. Some valid information about the system can be easily derived directly from this description, for example that some atomic propositions cannot be valid at the same time. The paper shows several ways to apply this information to improve the Büchi automaton built from an LTL specification. As a result, we get smaller automata with shorter edge labels that are easier to understand and, more importantly, for which the explicit model checking process performs better.

In Czech

Při používání explicitní metody ověřování modelu jsou systémy typicky popsány implicitně a úsporně. Z tohoto implicitního popisu však lze snadno vyčíst užitečné informace, například že některé atomické propozice nemohou platit naráz. Tato publikace ukazuje několik způsobů, jak pomocí takovéto informace zlepšit Büchiho automat vytvořený na základě požadované specifikace zadané formulí ligiky LTL. Výsledkem jsou často menší automaty s kratšími návěštími hran, které jsou nejen jednoduší pro porozumění, ale především které zrychlují proces ověřování modelu.

---

Links

GBP202/12/G061, research and development project	Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI) Investor: Czech Science Foundation
MUNI/A/1159/2014, interní kód MU	Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV. Investor: Masaryk University, Category A
MUNI/A/1206/2014, interní kód MU	Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU) Investor: Masaryk University, Category A