
TL;DR
This paper introduces a new must-testing preorder based on justness as the completeness criterion, using Petri nets with read arcs to model systems and connecting to fair failure preorder concepts.
Contribution
It defines a novel must-testing preorder using justness, characterizes it as the fair failure preorder, and applies Petri nets with read arcs to process algebra semantics.
Findings
The new must-testing preorder is incomparable with the traditional one.
It is the coarsest precongruence preserving linear time properties under justness.
Petri nets with read arcs effectively model process algebra with signals.
Abstract
The concept of must testing is naturally parametrised with a chosen completeness criterion, defining the complete runs of a system. Here I employ justness as this completeness criterion, instead of the traditional choice of progress. The resulting must-testing preorder is incomparable with the default one, and can be characterised as the fair failure preorder of Vogler. It also is the coarsest precongruence preserving linear time properties when assuming justness. As my system model I here employ Petri nets with read arcs. Through their Petri net semantics, this work applies equally well to process algebras. I provide a Petri net semantics for a standard process algebra extended with signals; the read arcs are necessary to capture those signals.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Petri Nets in System Modeling · Business Process Modeling and Analysis
