Evidence extraction from parameterised Boolean equation systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)

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.

LanguageEnglish
Title of host publicationProceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018)
Subtitle of host publicationOxford, UK, July 18, 2018.
EditorsChristoph Benzmüller, Jens Otten
PublisherCEUR-WS.org
Pages86-100
Number of pages15
StatePublished - 1 Jan 2018
Event3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics, (ARQNL 2018) - Oxford, United Kingdom
Duration: 18 Jul 201818 Jul 2018
http://ceur-ws.org/Vol-2095/

Publication series

NameCEUR Workshop Proceedings
Volume2095
ISSN (Print)1613-0073

Conference

Conference3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics, (ARQNL 2018)
Abbreviated titleARQNL2018
CountryUnited Kingdom
CityOxford
Period18/07/1818/07/18
Internet address

Fingerprint

Model checking
Feedback
Hardware

Cite this

Wesselink, W., & Willemse, T. A. C. (2018). Evidence extraction from parameterised Boolean equation systems. In C. Benzmüller, & J. Otten (Eds.), Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018): Oxford, UK, July 18, 2018. (pp. 86-100). (CEUR Workshop Proceedings; Vol. 2095). CEUR-WS.org.
Wesselink, Wieger ; Willemse, Tim A.C./ Evidence extraction from parameterised Boolean equation systems. Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018): Oxford, UK, July 18, 2018.. editor / Christoph Benzmüller ; Jens Otten. CEUR-WS.org, 2018. pp. 86-100 (CEUR Workshop Proceedings).
@inproceedings{88387b5ef7ea47c487a05a7247823e74,
title = "Evidence extraction from parameterised Boolean equation systems",
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.",
author = "Wieger Wesselink and Willemse, {Tim A.C.}",
year = "2018",
month = "1",
day = "1",
language = "English",
series = "CEUR Workshop Proceedings",
publisher = "CEUR-WS.org",
pages = "86--100",
editor = "Christoph Benzm{\"u}ller and Jens Otten",
booktitle = "Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018)",

}

Wesselink, W & Willemse, TAC 2018, Evidence extraction from parameterised Boolean equation systems. in C Benzmüller & J Otten (eds), Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018): Oxford, UK, July 18, 2018.. CEUR Workshop Proceedings, vol. 2095, CEUR-WS.org, pp. 86-100, 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics, (ARQNL 2018), Oxford, United Kingdom, 18/07/18.

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 proceedingConference contributionAcademicpeer-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 -

Wesselink W, Willemse TAC. Evidence extraction from parameterised Boolean equation systems. In Benzmüller C, Otten J, editors, Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018): Oxford, UK, July 18, 2018.. CEUR-WS.org. 2018. p. 86-100. (CEUR Workshop Proceedings).