Lazy Automata Techniques for WS1S

DOI10.1007/978-3-662-54577-5_24zbMath1452.03090arXiv1701.06282OpenAlexW2579934549MaRDI QIDQ3303905

Ondřej Lengál, Petr Janků, Tomáš Vojnar, Lukáš Holík, Tomáš Fiedor

Publication date: 5 August 2020

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

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

zbMATH Keywords

finite automatondecision procedurefree variableatomic formulaautomaton state

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25)

Related Items (2)

Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure ⋮ Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure

Uses Software

• MONA
• HIP
• Antichains
• Slide

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Array theory of bounded elements and its applications
• MONA IMPLEMENTATION SECRETS
• Antichain Algorithms for Finite Automata
• When Simulation Meets Antichains
• New Algorithm for Weak Monadic Second-Order Logic on Inductive Structures
• The Tree Width of Separation Logic with Recursive Definitions
• Nested Antichains for WS1S
• An Efficient Decision Procedure for Imperative Tree Data Structures
• Minimization of symbolic automata
• Decidable logics combining heap structures and data
• Antichains: A New Algorithm for Checking Universality of Finite Automata

This page was built for publication: Lazy Automata Techniques for WS1S