Extending temporal logics with data variable quantifications

DOI10.4230/LIPICS.FSTTCS.2014.253MaRDI QIDQ2978518zbMATH OpenFDO

Authors Fu Song, Zhilin Wu

Publication date 25 April 2017

Full work available at URL https://doi.org/10.4230/LIPICS.FSTTCS.2014.253

zbMATH Keywords

alternating register automatadata automatamodel checkingsatisfiabilitytemporal logics with variable quantifications

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• On temporal logics with data variable quantifications: decidability and complexity
• Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
• Complexity and expressivity of branching- and alternating-time temporal logics with finitely many variables
• Counting CTL
• Model checking systems and specifications with parameterized atomic propositions

Cited in

(5)

• An automata-theoretic approach to model-checking systems and specifications over infinite data domains
• Temporal logics on words with multiple data values
• On temporal logics with data variable quantifications: decidability and complexity
• Model checking systems and specifications with parameterized atomic propositions
• LTL with arithmetic and its applications in reasoning about hierarchical systems

This page was built for publication: Extending temporal logics with data variable quantifications

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