Well-structured transition systems everywhere!

DOI10.1016/S0304-3975(00)00102-XzbMath0973.68170OpenAlexW1967174286MaRDI QIDQ5941101

Philippe Schnoebelen, Alain Finkel

Publication date: 20 August 2001

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(00)00102-x

zbMATH Keywords

verificationinfinite systemswell-quasi-ordering

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (only showing first 100 items - show all)

Zeno, Hercules, and the Hydra ⋮ Structural Invariants for the Verification of Systems with Parameterized Architectures ⋮ The Subtrace Order and Counting First-Order Logic ⋮ Computing Parameterized Invariants of Parameterized Petri Nets ⋮ Unnamed Item ⋮ Dynamic Recursive Petri Nets ⋮ Fixed points and Noetherian topologies ⋮ Coverability and Termination in Recursive Petri Nets ⋮ Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems ⋮ Monotonic Abstraction for Programs with Dynamic Memory Heaps ⋮ Verification of data-aware process models: checking soundness of Data Petri nets ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Parametric Verification of Weighted Systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Tree Pattern Rewriting Systems ⋮ Discovery, Verification and Conformance of Workflows with Cancellation ⋮ On the Reachability Analysis of Acyclic Networks of Pushdown Systems ⋮ Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets ⋮ A Biologically Inspired Model with Fusion and Clonation of Membranes ⋮ Universal safety for timed Petri nets is PSPACE-complete ⋮ Model Checking TLR* Guarantee Formulas on Infinite Systems ⋮ An Automata-Theoretic Approach to the Reachability Analysis of RPPS Systems ⋮ Dynamic Networks of Timed Petri Nets ⋮ An Assertional Language for the Verification of Systems Parametric in Several Dimensions ⋮ Decidability properties for fragments of CHR ⋮ Event-Clock Visibly Pushdown Automata ⋮ On the Qualitative Analysis of Conformon P Systems ⋮ Unnamed Item ⋮ Occam's razor applied to the Petri net coverability problem ⋮ Unnamed Item ⋮ WQO dichotomy for 3-graphs ⋮ Clique-width and well-quasi-ordering of triangle-free graph classes ⋮ The ideal view on Rackoff's coverability technique ⋮ Nested Petri Nets for Adaptive Process Modeling ⋮ A Forward-Backward Abstraction Refinement Algorithm ⋮ A Language-Based Comparison of Extensions of Petri Nets with and without Whole-Place Operations ⋮ Theories of orders on the set of words ⋮ Unnamed Item ⋮ Forward analysis for WSTS, part I: completions ⋮ Decidability Results for Restricted Models of Petri Nets with Name Creation and Replication ⋮ On the expressive power of process interruption and compensation ⋮ Non axiomatisability of positive relation algebras with constants, via graph homomorphisms ⋮ The Reachability Problem over Infinite Graphs ⋮ The Parametric Complexity of Lossy Counter Machines ⋮ On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems ⋮ Model-checking Timed Temporal Logics ⋮ Automatic Verification of Directory-Based Consistency Protocols ⋮ How to Tackle Integer Weighted Automata Positivity ⋮ Unnamed Item ⋮ On the expressive power of recursion, replication and iteration in process calculi ⋮ On Petri Nets with Hierarchical Special Arcs ⋮ Coverability, Termination, and Finiteness in Recursive Petri Nets ⋮ Reachability problems on reliable and lossy queue automata ⋮ On the expressive power of movement and restriction in pure mobile ambients ⋮ Ideal Abstractions for Well-Structured Transition Systems ⋮ Forward analysis and model checking for trace bounded WSTS ⋮ Alternating two-way AC-tree automata ⋮ Model Checking Parameterized Systems ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ Reduction rules for reset/inhibitor nets ⋮ Well-structured languages ⋮ Learning to verify branching time properties ⋮ Complete symbolic reachability analysis using back-and-forth narrowing ⋮ Branch-well-structured transition systems and extensions ⋮ On selective unboundedness of VASS ⋮ Advances in parameterized verification of population protocols ⋮ Using well-structured transition systems to decide divergence for catalytic P systems ⋮ WQO is decidable for factorial languages ⋮ Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes ⋮ Petri Nets with Structured Data ⋮ Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols ⋮ On the verification of membrane systems with dynamic structure ⋮ SMT-based generation of symbolic automata ⋮ Handling infinitely branching well-structured transition systems ⋮ Theory of interaction ⋮ Parameterized verification of time-sensitive models of ad hoc network protocols ⋮ Exponential improvement of time complexity of model checking for multiagent systems with perfect recall ⋮ Well-abstracted transition systems: Application to FIFO automata. ⋮ Deciding safety properties in infinite-state pi-calculus via behavioural types ⋮ On termination and invariance for faulty channel machines ⋮ Alternating complexity of counting first-order logic for the subword order ⋮ Complete Abstractions and Subclassical Modal Logics ⋮ Population protocols: beyond runtime analysis ⋮ Deciding Structural Liveness of Petri Nets ⋮ An automata-theoretic approach to the verification of distributed algorithms ⋮ Termination detection for active objects ⋮ Spatial and behavioral types in the pi-calculus ⋮ Aeolus: a component model for the cloud ⋮ The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings ⋮ Parametrized automata simulation and application to service composition ⋮ The decidability of verification under PS 2.0 ⋮ Data flow analysis of asynchronous systems using infinite abstract domains ⋮ Run-time complexity bounds using squeezers ⋮ Multi-parameterised compositional verification of safety properties ⋮ Well-quasi-ordering versus clique-width

Cites Work

• An introduction to FIFO nets - monogeneous nets: a subclass of FIFO nets
• On permutative grammars generating context-free languages
• Characterizing finite Kripke structures in propositional temporal logic
• Recursivite et cônes rationnels fermés par intersection
• Reduction and covering of infinite reachability trees
• Symbolic model checking: \(10^{20}\) states and beyond
• Some decision problems related to the reachability problem for Petri nets
• Deciding bisimulation equivalences for a class of non-finite-state programs
• A theory of timed automata
• A note on well quasi-orderings for powersets
• Fifo nets without order deadlock
• Algorithmic analysis of programs with well quasi-ordered domains.
• Unreliable channels are easier to verify than perfect channels
• Verifying programs with unreliable channels
• Parallel program schemata
• The theory of well-quasi-ordering: a frequently discovered concept
• On Communicating Finite-State Machines
• Priority Networks of Communicating Finite State Machines
• Deciding properties of integral relational automata
• Undecidable verification problems for programs with unreliable channels
• Hybrid automata with finite bisimulations
• Ordering by Divisibility in Abstract Algebras
• Ensuring completeness of symbolic verification methods for infinite-state systems
• Infinite results
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Well-structured transition systems everywhere!