Abstract
Model checking is a technique for automatically assessing the quality of software and hardware systems and designs. Given a formalisation of both the system behaviour and the requirements the system should meet, a model checker returns either a yes or a no. In case the answer is not as expected, it is desirable to provide feedback to the user as to why this is the case. Providing such feedback, however, is not straightforward if the requirement is expressed in a highly expressive logic such as the modal µ-calculus, and when the decision problem is solved using intermediate formalisms. In this paper, we show how to extract witnesses and counterexamples from parameterised Boolean equation systems encoding the model checking problem for the first-order modal µ-calculus. We have implemented our technique in the modelling and analysis toolset mCRL2 and showcase our approach on a few illustrative examples.
| Language | English |
|---|---|
| Title of host publication | Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018) |
| Subtitle of host publication | Oxford, UK, July 18, 2018. |
| Editors | Christoph Benzmüller, Jens Otten |
| Publisher | CEUR-WS.org |
| Pages | 86-100 |
| Number of pages | 15 |
| State | Published - 1 Jan 2018 |
| Event | 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics, (ARQNL 2018) - Oxford, United Kingdom Duration: 18 Jul 2018 → 18 Jul 2018 http://ceur-ws.org/Vol-2095/ |
Publication series
| Name | CEUR Workshop Proceedings |
|---|---|
| Volume | 2095 |
| ISSN (Print) | 1613-0073 |
Conference
| Conference | 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics, (ARQNL 2018) |
|---|---|
| Abbreviated title | ARQNL2018 |
| Country | United Kingdom |
| City | Oxford |
| Period | 18/07/18 → 18/07/18 |
| Internet address |
Fingerprint
Cite this
}
Evidence extraction from parameterised Boolean equation systems. / Wesselink, Wieger; Willemse, Tim A.C.
Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018): Oxford, UK, July 18, 2018.. ed. / Christoph Benzmüller; Jens Otten. CEUR-WS.org, 2018. p. 86-100 (CEUR Workshop Proceedings; Vol. 2095).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
TY - GEN
T1 - Evidence extraction from parameterised Boolean equation systems
AU - Wesselink,Wieger
AU - Willemse,Tim A.C.
PY - 2018/1/1
Y1 - 2018/1/1
N2 - Model checking is a technique for automatically assessing the quality of software and hardware systems and designs. Given a formalisation of both the system behaviour and the requirements the system should meet, a model checker returns either a yes or a no. In case the answer is not as expected, it is desirable to provide feedback to the user as to why this is the case. Providing such feedback, however, is not straightforward if the requirement is expressed in a highly expressive logic such as the modal µ-calculus, and when the decision problem is solved using intermediate formalisms. In this paper, we show how to extract witnesses and counterexamples from parameterised Boolean equation systems encoding the model checking problem for the first-order modal µ-calculus. We have implemented our technique in the modelling and analysis toolset mCRL2 and showcase our approach on a few illustrative examples.
AB - Model checking is a technique for automatically assessing the quality of software and hardware systems and designs. Given a formalisation of both the system behaviour and the requirements the system should meet, a model checker returns either a yes or a no. In case the answer is not as expected, it is desirable to provide feedback to the user as to why this is the case. Providing such feedback, however, is not straightforward if the requirement is expressed in a highly expressive logic such as the modal µ-calculus, and when the decision problem is solved using intermediate formalisms. In this paper, we show how to extract witnesses and counterexamples from parameterised Boolean equation systems encoding the model checking problem for the first-order modal µ-calculus. We have implemented our technique in the modelling and analysis toolset mCRL2 and showcase our approach on a few illustrative examples.
UR - http://www.scopus.com/inward/record.url?scp=85049752576&partnerID=8YFLogxK
M3 - Conference contribution
T3 - CEUR Workshop Proceedings
SP - 86
EP - 100
BT - Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018)
PB - CEUR-WS.org
ER -