8 citations · 18 across the 10 of their papers we have counts for
14 papers
Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures
Stephane Demri, Karin Quaas
We introduce the class of tree constraint automata with data values in Z (equipped with the less than relation and equality predicates to constants) and we show that the nonemptine…
New Techniques for Universality in Unambiguous Register Automata
Wojciech Czerwiński, Antoine Mottet, Karin Quaas
Register automata are finite automata equipped with a finite set of registers ranging over the domain of some relational structure like or . Register…
Computing Branching Distances Using Quantitative Games
Uli Fahrenberg, Axel Legay, Karin Quaas
We lay out a general method for computing branching distances between labeled transition systems. We translate the quantitative games used for defining these distances to other, pa…
On the Containment Problem for Unambiguous Single-Register Automata with Guessing
Antoine Mottet, Karin Quaas
Register automata extend classical finite automata with a finite set of registers that can store data from an infinite data domain for later equality comparisons with data from an…
Effective Definability of the Reachability Relation in Timed Automata
Martin Fränzle, Karin Quaas, Mahsa Shirmohammadi +1
We give a new proof of the result of Comon and Jurski that the binary reachability relation of a timed automaton is definable in linear arithmetic.
The Containment Problem for Unambiguous Register Automata
Antoine Mottet, Karin Quaas
We investigate the complexity of the containment problem "Does hold?", where is an unambiguous register automaton and is an arbitrary register automato…
Synchronizing Data Words for Register Automata
Karin Quaas, Mahsa Shirmohammadi
Register automata (RAs) are finite automata extended with a finite set of registers to store and compare data from an infinite domain. We study the concept of synchronizing data wo…
Revisiting Reachability in Timed Automata
Karin Quaas, Mahsa Shirmohammadi, James Worrell
We revisit a fundamental result in real-time verification, namely that the binary reachability relation between configurations of a given timed automaton is definable in linear ari…
The Complexity of Flat Freeze LTL
Benedikt Bollig, Karin Quaas, Arnaud Sangnier
We consider the model-checking problem for freeze LTL on one-counter automata (OCA). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter…
Path Checking for MTL and TPTL over Data Words
Shiguang Feng, Markus Lohrey, Karin Quaas
Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are quantitative extensions of linear temporal logic, which are prominent and widely used in the verificat…
MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable
Karin Quaas
Parametric timed automata extend timed automata (Alur and Dill, 1991) in that they allow the specification of parametric bounds on the clock values. Since their introduction in 199…
Verification for Timed Automata extended with Unbounded Discrete Data Structures
Karin Quaas
We study decidability of verification problems for timed automata extended with unbounded discrete data structures. More detailed, we extend timed automata with a pushdown stack. I…
On the Expressiveness of TPTL and MTL over ω-Data Words
Claudia Carapelle, Shiguang Feng, Oliver Fernández Gil +1
Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent extensions of Linear Temporal Logic to specify properties about data languages. In this pape…
Kleene Algebras and Semimodules for Energy Problems
Zoltán Ésik, Uli Fahrenberg, Axel Legay +1
With the purpose of unifying a number of approaches to energy problems found in the literature, we introduce generalized energy automata. These are finite automata whose edges are…