The power of well-structured systems

DOI10.1007/978-3-642-40184-8_2MaRDI QIDQ2842095zbMATH OpenOpenAlexFDO

Authors Sylvain Schmitz, Philippe Schnoebelen

Publication date 12 August 2013

Published in CONCUR 2013 – Concurrency Theory (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1402.2908

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Well-structured systems, aka WSTSs, are computational models where the set of possible configurations is equipped with a well-quasi-ordering which is compatible with the transition relation between configurations. This structure supports generic decidability results that are important in verification and several other fields. This paper recalls the basic theory underlying well-structured systems and shows how two classic decision algorithms can be formulated as an exhaustive search for some "bad" sequences. This lets us describe new powerful techniques for the complexity analysis of WSTS algorithms. Recently, these techniques have been successful in precisely characterising the power, in a complexity-theoretical sense, of several important WSTS models like unreliable channel systems, monotonic counter machines, or networks of timed systems.

Recommendations

• Well-structured transition systems everywhere!
• Algorithmic analysis of programs with well quasi-ordered domains.
• scientific article; zbMATH DE number 6790161
• Ideal abstractions for well-structured transition systems
• Handling infinitely branching WSTS

Cited in

(25)

• Parameterized model checking of rendezvous systems
• Handling infinitely branching well-structured transition systems
• Attributed transition systems with hidden transitions
• Algorithmic analysis of programs with well quasi-ordered domains.
• Ordinal theory for expressiveness of well-structured transition systems
• Running time analysis of broadcast consensus protocols
• Coverability trees for Petri nets with unordered data
• Complexity hierarchies beyond elementary
• Ideal abstractions for well-structured transition systems
• Ordinal theory for expressiveness of well structured transition systems
• Well (and better) quasi-ordered transition systems
• The ideal approach to computing closed subsets in well-quasi-orderings
• scientific article; zbMATH DE number 4030997 (Why is no real title available?)
• Well structured transition systems with history
• The Parametric Complexity of Lossy Counter Machines
• SMT-based verification of data-aware processes: a model-theoretic approach
• Exhibition of a structural bug with wings
• Handling infinitely branching WSTS
• Expressive Power of Broadcast Consensus Protocols
• Parameterized broadcast networks with registers: from NP to the frontiers of decidability
• Analysis of the structure of attributed transition systems without hidden transitions
• Phase-bounded broadcast networks over topologies of communication
• Automatic WSTS-based repair and deadlock detection of parameterized systems
• Well-structured graph transformation systems
• Wait-only broadcast protocols are easier to verify

This page was built for publication: The power of well-structured systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2842095)