Algorithmic analysis of programs with well quasi-ordered domains.

DOI10.1006/inco.1999.2843zbMath1046.68567DBLPjournals/iandc/AbdullaCJT00OpenAlexW2052306562WikidataQ56901005 ScholiaQ56901005MaRDI QIDQ1854355

Kārlis Čerāns, Bengt Jonsson, Parosh Aziz Abdulla, Yih-Kuen Tsay

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1999.2843

zbMATH Keywords

decidability well-structured systems

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Related Items (47)

Reachability problems on reliable and lossy queue automata ⋮ Forward analysis and model checking for trace bounded WSTS ⋮ Unnamed Item ⋮ Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols ⋮ Branch-well-structured transition systems and extensions ⋮ Handling infinitely branching well-structured transition systems ⋮ Exponential improvement of time complexity of model checking for multiagent systems with perfect recall ⋮ Deciding safety properties in infinite-state pi-calculus via behavioural types ⋮ On termination and invariance for faulty channel machines ⋮ Complete Abstractions and Subclassical Modal Logics ⋮ Monotonic Abstraction for Programs with Dynamic Memory Heaps ⋮ Deciding Structural Liveness of Petri Nets ⋮ Unnamed Item ⋮ When Is Reachability Intrinsically Decidable? ⋮ The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings ⋮ Run-time complexity bounds using squeezers ⋮ Universal safety for timed Petri nets is PSPACE-complete ⋮ Forward Analysis and Model Checking for Trace Bounded WSTS ⋮ Multiply-Recursive Upper Bounds with Higman’s Lemma ⋮ Computable fixpoints in well-structured symbolic model checking ⋮ Ordinal recursive complexity of unordered data nets ⋮ Dynamic Networks of Timed Petri Nets ⋮ Hardness Results for Coverability Problem of Well-Structured Pushdown Systems ⋮ Decidability and complexity of Petri nets with unordered data ⋮ Well-structured transition systems everywhere! ⋮ Multiset rewriting for the verification of depth-bounded processes with name binding ⋮ Occam's razor applied to the Petri net coverability problem ⋮ A general approach to comparing infinite-state systems with their finite-state specifications ⋮ Clique-width and well-quasi-ordering of triangle-free graph classes ⋮ The ideal view on Rackoff's coverability technique ⋮ Handling Parameterized Systems with Non-atomic Global Conditions ⋮ Well (and Better) Quasi-Ordered Transition Systems ⋮ Deciding branching time properties for asynchronous programs ⋮ Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols ⋮ Coverability Trees for Petri Nets with Unordered Data ⋮ Unnamed Item ⋮ Forward analysis for WSTS, part I: completions ⋮ Decidability Results for Restricted Models of Petri Nets with Name Creation and Replication ⋮ The Parametric Complexity of Lossy Counter Machines ⋮ Complexity Hierarchies beyond Elementary ⋮ Unnamed Item ⋮ Structural liveness of Petri nets is \textsc{ExpSpace}-hard and decidable ⋮ Approximated parameterized verification of infinite-state processes with global conditions ⋮ Monotonic Abstraction in Action ⋮ Verifying lossy channel systems has nonprimitive recursive complexity. ⋮ Model checking of systems with many identical timed processes ⋮ On the Expressiveness of Mobile Synchronizing Petri Nets

Cites Work

This page was built for publication: Algorithmic analysis of programs with well quasi-ordered domains.