On the complexity of checking semantic equivalences between pushdown processes and finite-state processes

DOI10.1016/j.ic.2010.01.003zbMath1194.68162OpenAlexW2129121801MaRDI QIDQ988552

Richard Mayr, Antonín Kučera

Publication date: 18 August 2010

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

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/17903813/Kucera_Mayr_2010_On_the_Complexity_of_Checking_Semantic_Equivalences_between_Pushdown_Processes_and_Finite_State_Processes.pdf

zbMATH Keywords

verificationsimulationbisimulationpushdown automata

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

A generic framework for checking semantic equivalences between pushdown automata and finite-state automata ⋮ Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems ⋮ Unnamed Item ⋮ Deciding semantic finiteness of pushdown processes and first-order grammars w.r.t. bisimulation equivalence

Cites Work

• Undecidability of bisimilarity for Petri nets and some related problems
• Results on the propositional \(\mu\)-calculus
• A short proof of the decidability of bisimulation for normed BPA- processes
• The inclusion problem for simple languages
• Decidability of bisimulation equivalence for normed pushdown processes
• A polynomial algorithm for deciding bisimilarity of normed context-free processes
• Weak bisimilarity and regularity of context-free processes is EXPTIME-hard
• Pushdown processes: Games and model-checking
• Simulation preorder over simple process algebras
• Model checking LTL with regular valuations for pushdown systems
• Bisimulation equivalence is decidable for all context-free processes
• Decidability of model checking for infinite-state concurrent systems
• Decidability of bisimulation equivalence for process generating context-free languages
• Graphes canoniques de graphes algébriques
• Undecidability of bisimilarity by defender's forcing
• An elementary bisimulation decision procedure for arbitrary context-free processes
• Process Algebra
• Actions speak louder than words: proving bisimilarity for context-free processes
• Tools and Algorithms for the Construction and Analysis of Systems
• The Bisimulation Problem for Equational Graphs of Finite Out-Degree
• Equivalence-checking on infinite-state systems: Techniques and results
• Deciding bisimulation-like equivalences with finite-state processes
• Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time
• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item