On temporal logics with data variable quantifications: decidability and complexity

DOI10.1016/j.ic.2016.08.002zbMath1353.68181OpenAlexW2518211214MaRDI QIDQ342712

Fu Song, Zhilin Wu

Publication date: 18 November 2016

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2016.08.002

zbMATH Keywords

model checkingsatisfiabilityalternating register automatadata automatadata variable quantificationsdecidability and complexitytemporal logics

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

A Note on C² Interpreted over Finite Data-Words

Uses Software

• TeMP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On notions of regularity for data languages
• An automata-theoretic approach to constraint LTL
• Reasoning about networks with many identical finite state processes
• Using branching time temporal logic to synthesize synchronization skeletons
• Concerning the semantic consequence relation in first-order temporal logic
• A complete axiomatic characterization of first-order temporal logic of linear time
• Incompleteness of first-order temporal logic with until
• Finite-memory automata
• Context-free languages over infinite alphabets
• Decidable fragments of first-order temporal logics
• Automata, logics, and infinite games. A guide to current research
• On pebble automata for data languages with decidable emptiness problem
• On the universal and existential fragments of the \(\mu\)-calculus
• Tools and algorithms for the construction and analysis of systems. 20th international conference, TACAS 2014, held as part of the European joint conferences on theory and practice of software, ETAPS 2014, Grenoble, France, April 5--13, 2014. Proceedings
• Mechanising first-order temporal resolution
• On Freeze LTL with Ordered Attributes
• An extension of data automata that captures XPath
• Alternating register automata on finite words and trees
• Feasible Automata for Two-Variable Logic with Successor on Data Words
• Pushdown Model Checking for Malware Detection
• Temporal Logics on Words with Multiple Data Values.
• LTL with the freeze quantifier and register automata
• Two-variable logic on data words
• Algorithmic analysis of array-accessing programs
• Graph Reachability and Pebble Automata over Infinite Alphabets
• CLASS COUNTING AUTOMATA ON DATAWORDS
• FINITE-MEMORY AUTOMATA WITH NON-DETERMINISTIC REASSIGNMENT
• Ordered Navigation on Multi-attributed Data Words
• A Game-Theoretic Approach to Simulation of Data-Parameterized Systems
• Variable Automata over Infinite Alphabets
• Reasoning about systems with many processes
• Model Checking Systems and Specifications with Parameterized Atomic Propositions
• An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications
• Reasoning about Data Repetitions with Counter Systems
• Monodic temporal resolution
• Automated Reasoning
• LTL Model-Checking for Malware Detection
• An automata-theoretic approach to branching-time model checking
• Extending two-variable logic on data trees with order on data values and its automata
• On Reasoning About Rings

This page was built for publication: On temporal logics with data variable quantifications: decidability and complexity