A generic framework for checking semantic equivalences between pushdown automata and finite-state automata

DOI10.1016/j.jcss.2017.09.004zbMath1378.68106OpenAlexW1585666806MaRDI QIDQ2409577

Antonín Kučera, Richard Mayr

Publication date: 11 October 2017

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jcss.2017.09.004

zbMATH Keywords

bisimulationpushdown automatasemantic equivalences

Mathematics Subject Classification ID

Formal languages and automata (68Q45) 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 (1)

Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems

Cites Work

• 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
• On the complexity of checking semantic equivalences between pushdown processes and finite-state processes
• A short proof of the decidability of bisimulation for normed BPA- processes
• The inclusion problem for simple languages
• A polynomial algorithm for deciding bisimilarity of normed context-free processes
• The complexity of bisimilarity-checking for one-counter processes.
• \(L(A)=L(B)\)? decidability results from complete formal systems
• On finite representations of infinite-state behaviours
• Simulation preorder over simple process algebras
• Model checking LTL with regular valuations for pushdown systems
• Deciding branching bisimilarity of normed context-free processes ls in \(\sum_ 2^ p\)
• Bisimulation equivalence is decidable for all context-free processes
• Decidability of model checking for infinite-state concurrent systems
• BPA bisimilarity is EXPTIME-hard
• A general approach to comparing infinite-state systems with their finite-state specifications
• Simulation Problems Over One-Counter Nets
• Decidability of bisimulation equivalence for process generating context-free languages
• Graphes canoniques de graphes algébriques
• An elementary bisimulation decision procedure for arbitrary context-free processes
• Bisimilarity of One-Counter Processes Is PSPACE-Complete
• Process Algebra
• Actions speak louder than words: proving bisimilarity for context-free processes
• Branching time and abstraction in bisimulation semantics
• Branching Bisimilarity of Normed BPA Processes Is in NEXPTIME
• Branching Bisimilarity on Normed BPA Is EXPTIME-Complete
• A Logical Viewpoint on Process-algebraic Quotients
• Bisimulation Equivalence of First-Order Grammars
• Branching Bisimilarity Checking for PRS
• Bisimilarity of Pushdown Automata is Nonelementary
• Tools and Algorithms for the Construction and Analysis of Systems
• The Bisimulation Problem for Equational Graphs of Finite Out-Degree
• Checking Equality and Regularity for Normed BPA with Silent Moves
• Equivalences of Pushdown Systems Are Hard
• Equivalence-checking on infinite-state systems: Techniques and results
• Equivalence of deterministic one-counter automata is NL-complete
• Decidability of DPDA equivalence
• Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time
• Reachability analysis of pushdown automata: Application to model-checking
• Infinite results

This page was built for publication: A generic framework for checking semantic equivalences between pushdown automata and finite-state automata