Certifying inexpressibility

DOI10.1007/978-3-030-71995-1_20MaRDI QIDQ2233423zbMATH OpenOpenAlexFDO

Authors Orna Kupferman, Salomon Sickert

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2101.08756

zbMATH Keywords

gamesexpressive powerautomata on infinite words

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Cites work

• scientific article; zbMATH DE number 3990873 (Why is no real title available?)
• scientific article; zbMATH DE number 734956 (Why is no real title available?)
• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• scientific article; zbMATH DE number 1555955 (Why is no real title available?)
• scientific article; zbMATH DE number 1765703 (Why is no real title available?)
• scientific article; zbMATH DE number 3999901 (Why is no real title available?)
• scientific article; zbMATH DE number 2206109 (Why is no real title available?)
• scientific article; zbMATH DE number 3237829 (Why is no real title available?)
• Approximate automata for omega-regular languages
• Automata theory and model checking
• Beyond hyper-minimisation -- minimising DBAs and DPAs is NP-complete
• Büchi complementation made tight
• Certifying inexpressibility
• Counterexample-guided abstraction refinement for symbolic model checking
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Decision problems forω-automata
• Efficient minimization of deterministic weak -automata
• Efficient separability of regular languages by subsequences and suffixes
• Exponential Determinization for ω‐Automata with a Strong Fairness Acceptance Condition
• Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words
• Fixing the state budget: approximation of regular languages with small DFAs
• From linear time to branching time
• Graph Games and Reactive Synthesis
• Linear Automaton Transformations
• Modalities for model checking: Branching time logic strikes back
• Model checking probabilistic systems
• On bounded specifications
• On ω-regular sets
• Reasoning about infinite computations
• Recognizing safety and liveness
• Regular separability of well-structured transition systems
• Separating regular languages with first-order logic
• Solving Sequential Conditions by Finite-State Strategies
• Solving parity games: explicit vs symbolic
• TYPENESS FOR ω-REGULAR AUTOMATA
• Testing and generating infinite sequences by a finite automaton
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(4)

• Certifying inexpressibility
• The inexpressibility of validity
• Certifying DFA bounds for recognition and separation
• Impossibility of gathering, a certification

This page was built for publication: Certifying inexpressibility

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