Search Results

Documents authored by Willemse, Tim A. C.

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.38
Progress, Justness and Fairness in Modal μ-Calculus Formulae

Authors: Myrthe S. C. Spronck, Bas Luttik, and Tim A. C. Willemse

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
When verifying liveness properties on a transition system, it is often necessary to discard spurious violating paths by making assumptions on which paths represent realistic executions. Capturing that some property holds under such an assumption in a logical formula is challenging and error-prone, particularly in the modal μ-calculus. In this paper, we present template formulae in the modal μ-calculus that can be instantiated to a broad range of liveness properties. We consider the following assumptions: progress, justness, weak fairness, strong fairness, and hyperfairness, each with respect to actions. The correctness of these formulae has been proven.
Cite as

Myrthe S. C. Spronck, Bas Luttik, and Tim A. C. Willemse. Progress, Justness and Fairness in Modal μ-Calculus Formulae. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 38:1-38:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{spronck_et_al:LIPIcs.CONCUR.2024.38,
  author =	{Spronck, Myrthe S. C. and Luttik, Bas and Willemse, Tim A. C.},
  title =	{{Progress, Justness and Fairness in Modal \mu-Calculus Formulae}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{38:1--38:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.38},
  URN =		{urn:nbn:de:0030-drops-208102},
  doi =		{10.4230/LIPIcs.CONCUR.2024.38},
  annote =	{Keywords: Modal \mu-calculus, Property specification, Completeness criteria, Progress, Justness, Fairness, Liveness properties}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.4
The Best of Both Worlds: Model-Driven Engineering Meets Model-Based Testing

Authors: P. H. M. van Spaendonck and Tim A. C. Willemse

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We study the connection between stable-failures refinement and the ioco conformance relation. Both behavioural relations underlie methodologies that have gained traction in industry: stable-failures refinement is used in several commercial Model-Driven Engineering tool suites, whereas the ioco conformance relation is used in Model-Based Testing tools. Refinement-based Model-Driven Engineering approaches promise to generate executable code from high-level models, thus guaranteeing that the code upholds specified behavioural contracts. Manual testing, however, is still required to gain confidence that the model-to-code transformation and the execution platform do not lead to unexpected contract violations. We identify conditions under which also this last step in the design methodology can be automated using the ioco conformance relation and the associated tools.
Cite as

P. H. M. van Spaendonck and Tim A. C. Willemse. The Best of Both Worlds: Model-Driven Engineering Meets Model-Based Testing. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{vanspaendonck_et_al:LIPIcs.CONCUR.2023.4,
  author =	{van Spaendonck, P. H. M. and Willemse, Tim A. C.},
  title =	{{The Best of Both Worlds: Model-Driven Engineering Meets Model-Based Testing}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{4:1--4:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.4},
  URN =		{urn:nbn:de:0030-drops-189988},
  doi =		{10.4230/LIPIcs.CONCUR.2023.4},
  annote =	{Keywords: stable-failures refinement, Model-Driven Engineering, input output conformance, Input Output Labelled Transition Systems, internal choice}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.28
Real Equation Systems with Alternating Fixed-Points

Authors: Jan Friso Groote and Tim A. C. Willemse

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We introduce the notion of a Real Equation System (RES), which lifts Boolean Equation Systems (BESs) to the domain of extended real numbers. Our RESs allow arbitrary nesting of least and greatest fixed-point operators. We show that each RES can be rewritten into an equivalent RES in normal form. These normal forms provide the basis for a complete procedure to solve RESs. This employs the elimination of the fixed-point variable at the left side of an equation from its right-hand side, combined with a technique often referred to as Gauß-elimination. We illustrate how this framework can be used to verify quantitative modal formulas with alternating fixed-point operators interpreted over probabilistic labelled transition systems.
Cite as

Jan Friso Groote and Tim A. C. Willemse. Real Equation Systems with Alternating Fixed-Points. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{groote_et_al:LIPIcs.CONCUR.2023.28,
  author =	{Groote, Jan Friso and Willemse, Tim A. C.},
  title =	{{Real Equation Systems with Alternating Fixed-Points}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{28:1--28:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.28},
  URN =		{urn:nbn:de:0030-drops-190225},
  doi =		{10.4230/LIPIcs.CONCUR.2023.28},
  annote =	{Keywords: Real Equation System, Solution method, Gau{\ss}-elimination, Model checking, Quantitative modal mu-calculus}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.78
Evidence for Fixpoint Logic

Authors: Sjoerd Cranen, Bas Luttik, and Tim A. C. Willemse

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
For many modal logics, dedicated model checkers offer diagnostics (e.g., counterexamples) that help the user understand the result provided by the solver. Fixpoint logic offers a unifying framework in which such problems can be expressed and solved, but a drawback of this framework is that it lacks comprehensive diagnostics generation. We extend the framework with a notion of evidence, which can be specialized to obtain diagnostics for various model checking problems, behavioural equivalence and refinement checking problems. We demonstrate this by showing how our notion of evidence can be used to obtain diagnostics for the problem of deciding stuttering bisimilarity. Moreover, we show that our notion generalizes the existing notions of counterexample and witness for LTL and ACTL* model checking.
Cite as

Sjoerd Cranen, Bas Luttik, and Tim A. C. Willemse. Evidence for Fixpoint Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 78-93, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cranen_et_al:LIPIcs.CSL.2015.78,
  author =	{Cranen, Sjoerd and Luttik, Bas and Willemse, Tim A. C.},
  title =	{{Evidence for Fixpoint Logic}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{78--93},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.78},
  URN =		{urn:nbn:de:0030-drops-54080},
  doi =		{10.4230/LIPIcs.CSL.2015.78},
  annote =	{Keywords: fixpoint logic, diagnostics, counterexample, model checking, stuttering bisimilarity, ACTL*}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact