6,076 research outputs found
Off-the-Shelf Automated Analysis of Liveness Properties for Just Paths
Full text linkRecent work by van Glabbeek and coauthors suggests that the liveness property for Peterson’s mutual exclusion algorithm, which states that any process wanting to enter the critical section will eventually enter it, cannot be analysed in CCS and related formalisms. In our article, we explore the formal underpinning of this suggestion and its ramifications. In particular, we show that the liveness property for Peterson’s algorithm can be established convincingly with the mCRL2 toolset, which has a conventional ACP-style process-algebra based specification formalism.</p
Infinite-data PBES Quotienting with the mCRL2 toolset
No full textThis folder contains the benchmarks that were performed as part of the publications
Thomas Neele, Tim A. C. Willemse, Jan Friso Groote:
Solving Parameterised Boolean Equation Systems with Infinite Data Through Quotienting.
FACS 2018. LNCS 11222, pp. 216-236.
and
Thomas Neele, Tim A. C. Willemse, Jan Friso Groote:
Finding Compact Proofs for Infinite-Data Parameterised Boolean Equation Systems.
Science of Computer Programming, FACS 2018 special issue. Accepted for publication.</p
Games for Bisimulation and Abstraction
Full text linkContains fulltext :
181620.pdf (Publisher’s version ) (Open Access
Dataset with experiments for 'Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems'
No full textThis archive contains the experiments that were performed as part of the publication
Thomas Neele, Tim A. C. Willemse, Wieger Wesselink: Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems.
TACAS 2020 (accepted for publication).</p
Infinite-data PBES Quotienting with the mCRL2 toolset
No full textThis folder contains the benchmarks that were performed as part of the publications Thomas Neele, Tim A. C. Willemse, Jan Friso Groote: Solving Parameterised Boolean Equation Systems with Infinite Data Through Quotienting. FACS 2018. LNCS 11222, pp. 216-236. and Thomas Neele, Tim A. C. Willemse, Jan Friso Groote: Finding Compact Proofs for Infinite-Data Parameterised Boolean Equation Systems. Science of Computer Programming (FACS 2018 special issue), vol. 188, 102389, 2020
A symmetric protocol to establish service level agreements
Full text linkWe present a symmetrical protocol to repeatedly negotiate a desired service level between two parties, where the service levels are taken from some totally ordered finite domain. The agreed service level is selected from levels dynamically proposed by both parties and parties can only decrease the desired service level during a negotiation. The correctness of the protocol is stated using modal formulas and its behaviour is explained using behavioural reductions of the external behaviour modulo weak trace equivalence and divergence-preserving branching bisimulation. Our protocol originates from an industrial use case and it turned out to be remarkably tricky to design correctly
Review of: Roberto Calasso (Translator: Tim Parks),<i>The Tablet of Destinies</i>, Farrar, New York: Straus and Giroux 2022 (113 p.)
No full textReal Equation Systems with Alternating Fixed-Points
Full text linkWe 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
Evidence for Fixpoint Logic
Full text linkFor 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
- …
