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

DOI10.1016/J.IC.2010.01.003MaRDI QIDQ988552zbMATH OpenOpenAlexFDO

Authors Antonin Kučera, Richard M. Mayr

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

verificationsimulationpushdown automatabisimulation

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1929958
• A generic framework for checking semantic equivalences between pushdown automata and finite-state automata
• scientific article; zbMATH DE number 2163034
• Simulation preorder over simple process algebras
• scientific article; zbMATH DE number 1696434

Cites work

• scientific article; zbMATH DE number 5604065 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 3688686 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 47903 (Why is no real title available?)
• scientific article; zbMATH DE number 1222559 (Why is no real title available?)
• scientific article; zbMATH DE number 1361117 (Why is no real title available?)
• scientific article; zbMATH DE number 1361133 (Why is no real title available?)
• scientific article; zbMATH DE number 2038739 (Why is no real title available?)
• scientific article; zbMATH DE number 2080197 (Why is no real title available?)
• scientific article; zbMATH DE number 1927587 (Why is no real title available?)
• scientific article; zbMATH DE number 1927588 (Why is no real title available?)
• scientific article; zbMATH DE number 1754582 (Why is no real title available?)
• scientific article; zbMATH DE number 1759489 (Why is no real title available?)
• scientific article; zbMATH DE number 1796135 (Why is no real title available?)
• scientific article; zbMATH DE number 1796143 (Why is no real title available?)
• scientific article; zbMATH DE number 2163034 (Why is no real title available?)
• scientific article; zbMATH DE number 2086665 (Why is no real title available?)
• A polynomial algorithm for deciding bisimilarity of normed context-free processes
• A short proof of the decidability of bisimulation for normed BPA- processes
• Actions speak louder than words: proving bisimilarity for context-free processes
• An elementary bisimulation decision procedure for arbitrary context-free processes
• Bisimulation equivalence is decidable for all context-free processes
• Decidability of bisimulation equivalence for normed pushdown processes
• Decidability of bisimulation equivalence for process generating context-free languages
• Decidability of model checking for infinite-state concurrent systems
• Deciding bisimulation-like equivalences with finite-state processes
• Equivalence-checking on infinite-state systems: Techniques and results
• Graphes canoniques de graphes algébriques
• Model checking LTL with regular valuations for pushdown systems
• Process Algebra
• Pushdown processes: Games and model-checking
• Results on the propositional \(\mu\)-calculus
• Simulation preorder over simple process algebras
• The Bisimulation Problem for Equational Graphs of Finite Out-Degree
• The inclusion problem for simple languages
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
• Tools and Algorithms for the Construction and Analysis of Systems
• Undecidability of bisimilarity by defender's forcing
• Undecidability of bisimilarity for Petri nets and some related problems
• Verification on infinite structures.
• Weak bisimilarity and regularity of context-free processes is EXPTIME-hard
• Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time

Cited in

(13)

• Deciding semantic finiteness of pushdown processes and first-order grammars w.r.t. bisimulation equivalence
• scientific article; zbMATH DE number 2163034 (Why is no real title available?)
• Deciding Semantic Finiteness of Pushdown Processes and First-Order Grammars w.r.t. Bisimulation Equivalence.
• A direct branching algorithm for checking the equivalence of two deterministic pushdown transducers, one of which is real-time strict
• A generic framework for checking semantic equivalences between pushdown automata and finite-state automata
• Game characterization of probabilistic bisimilarity, and applications to pushdown automata
• Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems
• Hardness of preorder checking for basic formalisms
• Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation
• Hardness of preorder checking for basic formalisms
• scientific article; zbMATH DE number 1696434 (Why is no real title available?)
• scientific article; zbMATH DE number 1929958 (Why is no real title available?)
• Checking equivalences between concurrent systems of finite agents (extended abstract)

This page was built for publication: On the complexity of checking semantic equivalences between pushdown processes and finite-state processes

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