On the complexity of the linear-time μ-calculus for Petri Nets

DOI10.1007/3-540-63139-9_32MaRDI QIDQ6487371zbMATH OpenFDO

Authors Peter Habermehl

Publication date 9 December 2022

Full work available at URL https://doi.org/10.1007/3-540-63139-9_32

Mathematics Subject Classification ID

Temporal logic (03B44) 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)

Recommendations

• scientific article; zbMATH DE number 2217747
• scientific article; zbMATH DE number 1456956
• Decidability of model checking for infinite-state concurrent systems
• scientific article; zbMATH DE number 1263840
• Applications and Theory of Petri Nets 2004

Cites work

• A multiparameter analysis of the boundedness problem for vector addition systems
• Bounds on Positive Integral Solutions of Linear Diophantine Equations
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 1318521 (Why is no real title available?)
• scientific article; zbMATH DE number 1860681 (Why is no real title available?)
• scientific article; zbMATH DE number 1456956 (Why is no real title available?)
• Infinite results
• Reasoning about infinite computations
• Relationships between nondeterministic and deterministic tape complexities
• Temporal logic can be more expressive
• The covering and boundedness problems for vector addition systems
• Verifying programs with unreliable channels

Cited in

(14)

• Strategic reasoning with a bounded number of resources: the quest for tractability
• Model checking for process rewrite systems and a class of action-based regular properties
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Reasoning about equilibria in game-like concurrent systems
• On selective unboundedness of VASS
• scientific article; zbMATH DE number 1456956 (Why is no real title available?)
• Forward analysis for WSTS. III: Karp-Miller trees
• scientific article; zbMATH DE number 2217747 (Why is no real title available?)
• On the complexity of resource-bounded logics
• Reasoning about reversal-bounded counter machines
• Separability in Büchi VASS and singly nonlinear systems of inequalities
• Wait-only broadcast protocols are easier to verify
• EXPSPACE lower bounds for the simulation preorder between a communication-free Petri net and a finite-state system

This page was built for publication: On the complexity of the linear-time μ-calculus for Petri Nets

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