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

DOI10.1016/J.JCSS.2017.09.004zbMATH Open1378.68106OpenAlexW1585666806MaRDI QIDQ2409577FDOQ2409577

Antonin Kučera, Richard M. 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

Recommendations

• scientific article; zbMATH DE number 2163034
• On the complexity of checking semantic equivalences between pushdown processes and finite-state processes
• Equivalence of deterministic pushdown automata revisited
• Equivalence checking problem for finite state transducers over semigroups
• An extended direct branching algorithm for checking equivalence of deterministic pushdown automata
• On Equivalence Checking of Nondeterministic Finite Automata
• scientific article; zbMATH DE number 1929958
• Reachability analysis of pushdown automata: Application to model-checking
• Equivalence of pushdown automata via first-order grammars
• A direct branching algorithm for checking equivalence of some classes of deterministic pushdown automata

zbMATH Keywords

pushdown automatabisimulationsemantic 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)

Cites Work

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

Cited In (5)

• Title not available (Why is that?)
• A direct branching algorithm for checking equivalence of some classes of deterministic pushdown automata
• Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems
• Title not available (Why is that?)
• Generalizations of checking stack automata: characterizations and hierarchies

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

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