Search

• < Previous
• 1
• Next >

---

A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction

Thomas Neele ; Antti Valmari ; Tim A. C. Willemse.

One of the most popular state-space reduction techniques for model checking is partial-order reduction (POR). Of the many different POR implementations, stubborn sets are a very versatile variant and have thus seen many different applications over the past 32 years. One of the early stubborn sets&nbsp;[&hellip;]

---

A symmetric protocol to establish service level agreements

Jan Friso Groote ; Tim A. C. Willemse.

We 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&nbsp;[&hellip;]

---

Correct and Efficient Antichain Algorithms for Refinement Checking

Maurice Laveaux ; Jan Friso Groote ; Tim A. C. Willemse.

The notion of refinement plays an important role in software engineering. It is the basis of a stepwise development methodology in which the correctness of a system can be established by proving, or computing, that a system refines its specification. Wang et al. describe algorithms based on&nbsp;[&hellip;]

---

Games for Bisimulations and Abstraction

David De Frutos Escrig ; Jeroen J. A. Keiren ; Tim A. C. Willemse.

Weak bisimulations are typically used in process algebras where silent steps are used to abstract from internal behaviours. They facilitate relating implementations to specifications. When an implementation fails to conform to its specification, pinpointing the root cause can be challenging. In this&nbsp;[&hellip;]

---