Constraint automata on infinite data trees: from CTL(Z)/CTL^*(Z) to decision procedures
From MaRDI portal
Publication:6960758
Cites work
- A CTL* Model Checker for Petri Nets
- A generic solution to register-bounded synthesis with an application to discrete orders
- A tableau algorithm for description logics with concrete domains and general TBoxes
- Alternating automata modulo first order theories
- Alternating automata on data trees and XPath satisfiability
- Alternating timed automata
- An automata-based approach for \(\text{CTL}^{*}\) with constraints
- An automata-theoretic approach to branching-time model checking
- An automata-theoretic approach to constraint LTL
- Automata based verification over linearly ordered data domains
- Automata-theoretic techniques for modal logics of programs
- Boolean abstractions for realizability modulo theories
- Branching-time model checking gap-order constraint systems
- Branching-time model checking gap-order constraint systems
- Branching-time model checking of parametric one-counter automata
- Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
- Combining interval-based temporal reasoning with general TBoxes
- Computer Science Logic
- Constraint automata on infinite data trees: from CTL\((\mathbb{Z})\text{CTL}^*(\mathbb{Z})\) to decision procedures
- Counting in trees
- CTL* model checking for data-aware dynamic systems with arithmetic
- Decidability of downward XPath
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Deciding emptiness for constraint automata on strings with the prefix and suffix order
- Deciding full branching time logic
- Deciding properties of integral relational automata
- Finite state machines for strings over infinite alphabets
- First steps towards taming description logics with strings
- scientific article; zbMATH DE number 5872401 (Why is no real title available?)
- scientific article; zbMATH DE number 1303726 (Why is no real title available?)
- scientific article; zbMATH DE number 1142314 (Why is no real title available?)
- scientific article; zbMATH DE number 6902582 (Why is no real title available?)
- scientific article; zbMATH DE number 2086598 (Why is no real title available?)
- scientific article; zbMATH DE number 2196595 (Why is no real title available?)
- scientific article; zbMATH DE number 7646025 (Why is no real title available?)
- Introduction to constraint databases
- Logics of repeating values on data trees and branching counter systems
- LTL with the freeze quantifier and register automata
- Modal -calculus with atoms
- Model checking flat Freeze LTL on one-counter automata
- Model-checking parametric lock-sharing systems against regular constraints
- NExpTime-complete description logics with concrete domains
- On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
- On temporal logics with data variable quantifications: decidability and complexity
- On the complexity of model-checking branching and alternating-time temporal logics in one-counter systems
- Ordered navigation on multi-attributed data words
- Playing with repetitions in data words using energy games
- Presburger Büchi tree automata with applications to logics with expressive counting
- Realizability modulo theories
- Realizability problem for constraint LTL
- Reasoning about infinite computations
- Register automata with extrema constraints, and an application to two-variable logic
- Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints
- Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
- Speeding up the constraint-based method in difference logic
- Temporal constraint networks
- Temporal logics on strings with prefix relation
- The Complexity of Tree Automata and Logics of Programs
- Using model theory to find decidable and tractable description logics with concrete domains
- Verification of gap-order constraint abstractions of counter systems
- Verification of qualitative \(\mathbb Z\) constraints
- Why These Automata Types?
- “Sometimes” and “not never” revisited
This page was built for publication: Constraint automata on infinite data trees: from \(\mathrm{CTL}(\mathbb{Z})/\mathrm{CTL}^*(\mathbb{Z})\) to decision procedures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6960758)
