Creating Büchi automata for multi-valued model checking

Stefan J.J. Vijzelaar; Wan J. Fokkink

doi:10.1007/978-3-319-60225-7_15

Creating Büchi automata for multi-valued model checking

Stefan J.J. Vijzelaar^*, Wan J. Fokkink

^*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

21 Downloads (Pure)

Abstract

In explicit state model checking of linear temporal logic properties, a Büchi automaton encodes a temporal property. It interleaves with a Kripke model to form a state space, which is searched for counterexamples. Multi-valued model checking considers additional truth values beyond the Boolean true and false; these values add extra information to the model, e.g. for the purpose of abstraction or execution steering. This paper presents a method to create Büchi automata for multi-valued model checking using quasi-Boolean logics. It allows for multi-valued propositions as well as multi-valued transitions. A logic for the purpose of execution steering and abstraction is presented as an application.

Original language	English
Title of host publication	Formal Techniques for Distributed Objects, Components, and Systems
Subtitle of host publication	37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings
Editors	Ahmed Bouajjani, Alexandra Silva
Publisher	Springer/Verlag
Pages	210-224
Number of pages	15
ISBN (Electronic)	9783319602257
ISBN (Print)	9783319602240
DOIs	https://doi.org/10.1007/978-3-319-60225-7_15
Publication status	Published - 2017
Event	37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2017 - Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017 - Neuchatel, Switzerland Duration: 19 Jun 2017 → 22 Jun 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10321 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2017 - Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017
Country/Territory	Switzerland
City	Neuchatel
Period	19/06/17 → 22/06/17

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/978-3-319-60225-7_15

Creating Büchi Automata for Multi-valued Model CheckingFinal published version, 294 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

Cite this

Vijzelaar, S. J. J., & Fokkink, W. J. (2017). Creating Büchi automata for multi-valued model checking. In A. Bouajjani, & A. Silva (Eds.), Formal Techniques for Distributed Objects, Components, and Systems: 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings (pp. 210-224). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10321 LNCS). Springer/Verlag. https://doi.org/10.1007/978-3-319-60225-7_15

Vijzelaar, Stefan J.J. ; Fokkink, Wan J. / Creating Büchi automata for multi-valued model checking. Formal Techniques for Distributed Objects, Components, and Systems: 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings. editor / Ahmed Bouajjani ; Alexandra Silva. Springer/Verlag, 2017. pp. 210-224 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{b760e7a846c44be4a59b78b1dbd2fcb5,

title = "Creating B{\"u}chi automata for multi-valued model checking",

abstract = "In explicit state model checking of linear temporal logic properties, a B{\"u}chi automaton encodes a temporal property. It interleaves with a Kripke model to form a state space, which is searched for counterexamples. Multi-valued model checking considers additional truth values beyond the Boolean true and false; these values add extra information to the model, e.g. for the purpose of abstraction or execution steering. This paper presents a method to create B{\"u}chi automata for multi-valued model checking using quasi-Boolean logics. It allows for multi-valued propositions as well as multi-valued transitions. A logic for the purpose of execution steering and abstraction is presented as an application.",

author = "Vijzelaar, {Stefan J.J.} and Fokkink, {Wan J.}",

year = "2017",

doi = "10.1007/978-3-319-60225-7_15",

language = "English",

isbn = "9783319602240",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer/Verlag",

pages = "210--224",

editor = "Ahmed Bouajjani and Alexandra Silva",

booktitle = "Formal Techniques for Distributed Objects, Components, and Systems",

note = "37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2017 - Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017 ; Conference date: 19-06-2017 Through 22-06-2017",

}

Vijzelaar, SJJ & Fokkink, WJ 2017, Creating Büchi automata for multi-valued model checking. in A Bouajjani & A Silva (eds), Formal Techniques for Distributed Objects, Components, and Systems: 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10321 LNCS, Springer/Verlag, pp. 210-224, 37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2017 - Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchatel, Switzerland, 19/06/17. https://doi.org/10.1007/978-3-319-60225-7_15

Creating Büchi automata for multi-valued model checking. / Vijzelaar, Stefan J.J.; Fokkink, Wan J.
Formal Techniques for Distributed Objects, Components, and Systems: 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings. ed. / Ahmed Bouajjani; Alexandra Silva. Springer/Verlag, 2017. p. 210-224 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10321 LNCS).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Creating Büchi automata for multi-valued model checking

AU - Vijzelaar, Stefan J.J.

AU - Fokkink, Wan J.

PY - 2017

Y1 - 2017

N2 - In explicit state model checking of linear temporal logic properties, a Büchi automaton encodes a temporal property. It interleaves with a Kripke model to form a state space, which is searched for counterexamples. Multi-valued model checking considers additional truth values beyond the Boolean true and false; these values add extra information to the model, e.g. for the purpose of abstraction or execution steering. This paper presents a method to create Büchi automata for multi-valued model checking using quasi-Boolean logics. It allows for multi-valued propositions as well as multi-valued transitions. A logic for the purpose of execution steering and abstraction is presented as an application.

AB - In explicit state model checking of linear temporal logic properties, a Büchi automaton encodes a temporal property. It interleaves with a Kripke model to form a state space, which is searched for counterexamples. Multi-valued model checking considers additional truth values beyond the Boolean true and false; these values add extra information to the model, e.g. for the purpose of abstraction or execution steering. This paper presents a method to create Büchi automata for multi-valued model checking using quasi-Boolean logics. It allows for multi-valued propositions as well as multi-valued transitions. A logic for the purpose of execution steering and abstraction is presented as an application.

UR - http://www.scopus.com/inward/record.url?scp=85020493118&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85020493118&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-60225-7_15

DO - 10.1007/978-3-319-60225-7_15

M3 - Conference contribution

AN - SCOPUS:85020493118

SN - 9783319602240

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 210

EP - 224

BT - Formal Techniques for Distributed Objects, Components, and Systems

A2 - Bouajjani, Ahmed

A2 - Silva, Alexandra

PB - Springer/Verlag

T2 - 37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2017 - Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017

Y2 - 19 June 2017 through 22 June 2017

ER -

Vijzelaar SJJ, Fokkink WJ. Creating Büchi automata for multi-valued model checking. In Bouajjani A, Silva A, editors, Formal Techniques for Distributed Objects, Components, and Systems: 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings. Springer/Verlag. 2017. p. 210-224. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2017 Jun 6. doi: 10.1007/978-3-319-60225-7_15

Creating Büchi automata for multi-valued model checking

Abstract

Publication series

Conference

UN SDGs

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this