Well Behaved Transition Systems

TL;DR

This paper introduces well behaved transition systems (WBTS), a broader class than well-structured transition systems (WSTS), showing that coverability remains decidable under weaker conditions, thus expanding the scope of decidability in transition system analysis.

Contribution

The paper demonstrates that the well-quasi-ordering assumption in WSTS can be relaxed to allow more orderings, defining WBTS and proving coverability decidability under these weaker conditions.

Findings

Coverability is decidable for WBTS with no infinite antichains.

Boundedness and termination remain undecidable for WBTS.

Stronger monotonicity conditions can ensure decidability.

Abstract

The well-quasi-ordering (i.e., a well-founded quasi-ordering such that all antichains are finite) that defines well-structured transition systems (WSTS) is shown not to be the weakest hypothesis that implies decidability of the coverability problem. We show coverability decidable for monotone transition systems that only require the absence of infinite antichains and call well behaved transitions systems (WBTS) the new strict superclass of the class of WSTS that arises. By contrast, we confirm that boundedness and termination are undecidable for WBTS under the usual hypotheses, and show that stronger monotonicity conditions can enforce decidability. Proofs are similar or even identical to existing proofs but the surprising message is that a hypothesis implicitely assumed minimal for twenty years in the theory of WSTS can meaningfully be relaxed, allowing more orderings to be handled in an abstract way.