Logic programming approach to automata-based decision procedures

DOI10.1016/j.jlamp.2016.02.005zbMath1353.68039OpenAlexW2334804121MaRDI QIDQ347398

David Toman, Gulay Unel

Publication date: 30 November 2016

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2016.02.005

zbMATH Keywords

automatacomplex-value Datalog \((\text{Datalog}^{\text{cv}})\)magic setsSLG-resolutionWS1SWS2S

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) Logic programming (68N17)

Uses Software

• MONA
• LTL2BA
• XSB
• Slide
• MSO_Regex_Equivalence

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An automata theoretic decision procedure for the propositional mu- calculus
• Reasoning about infinite computations
• Automata, logics, and infinite games. A guide to current research
• MONA IMPLEMENTATION SECRETS
• On the power of magic
• Set constructors in a logic database language
• Weak Second‐Order Arithmetic and Finite Automata
• Deciding Entailments in Inductive Separation Logic with Tree Automata
• Automata for the modal μ-calculus and related results
• The Description Logic Handbook
• Logic Programming Approach to Automata-Based Decision Procedures
• BDD-based decision procedures for the modal logic K ★
• Deciding full branching time logic
• Decision Problems of Finite Automata Design and Related Arithmetics
• Alternating automata: Unifying truth and validity checking for temporal logics
• An automata-theoretic approach to branching-time model checking
• Generalized finite automata theory with an application to a decision problem of second-order logic
• Testing and generating infinite sequences by a finite automaton
• Decidability of Second-Order Theories and Automata on Infinite Trees
• A Decision Procedure for CTL* Based on Tableaux and Automata
• On model checking for the \(\mu\)-calculus and its fragments

This page was built for publication: Logic programming approach to automata-based decision procedures