449 research outputs found
A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains
Full text linkThis article improves the time bound for calculating the weak/branching bisimulation minimisation quotient on state-labelled discrete-time Markov chains from O(m n) to an expected-time O(m log⁴ n), where n is the number of states and m the number of transitions. For these results we assume that the set of state labels AP is small (|AP| ∈ O(m/n log⁴ n)). It follows the ideas of Groote et al. (ACM ToCL 2017) in combination with an efficient algorithm to handle decremental strongly connected components (Bernstein et al., STOC 2019)
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
Applications:Puzzles and Games
No full textMany puzzles can very naturally be described in mCRL2 and solved using the available analysis techniques such as model-checking. In this chapter, six different puzzles are specified and solved.</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
Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable
Full text linkWe study the problem of computing minimal distinguishing formulas for non-bisimilar states in finite LTSs. We show that this is NP-hard if the size of the formula must be minimal. Similarly, the existence of a short distinguishing trace is NP-complete. However, we can provide polynomial algorithms, if minimality is formulated as the minimal number of nested modalities, and it can even be extended by recursively requiring a minimal number of nested negations. A prototype implementation shows that the generated formulas are much smaller than those generated by the method introduced by Cleaveland
De kans om Ganzenbord te winnen
No full textIn dit artikel analyseren Jan Friso Groote en Hans Zantema de kans op winst voor de verschillende spelers van het traditionele bordspel Ganzenbord. Deze kansen kan men berekenen voor maximaal vijf spelers, waarbij het aantal toestanden oploopt tot zeer grote omvang. Voor twee spelers kan men deze kansen exact uitrekenen als breuken waarvan de tellers en noemers uit duizenden cijfers bestaan. Een verrassend resultaat is dat bij twee spelers de kans op gelijk spel (een speler in de put en de ander in de gevangenis) substantieel is: bijna 23 procent
Bisimulation by Partitioning Is Ω((m+n)log n)
Full text linkAn asymptotic lowerbound of Ω((m+n)log n) is established for partition refinement algorithms that decide bisimilarity on labeled transition systems. The lowerbound is obtained by subsequently analysing two families of deterministic transition systems - one with a growing action set and another with a fixed action set.
For deterministic transition systems with a one-letter action set, bisimilarity can be decided with fundamentally different techniques than partition refinement. In particular, Paige, Tarjan, and Bonic give a linear algorithm for this specific situation. We show, exploiting the concept of an oracle, that the approach of Paige, Tarjan, and Bonic is not of help to develop a generic algorithm for deciding bisimilarity on labeled transition systems that is faster than the established lowerbound of Ω((m+n)log n)
Real 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
- …
