Path Checking for MTL and TPTL over Data Words
DOI10.1007/978-3-319-21500-6_26zbMath1434.68297arXiv1412.3644OpenAlexW2962748292MaRDI QIDQ3451113
Markus Lohrey, Karin Quaas, Shiguang Feng
Publication date: 10 November 2015
Published in: Developments in Language Theory (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1412.3644
metric temporal logicdata wordsfreeze LTLdeterministic one-counter machinespath checking problemtimes propositional temporal logic
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)
Related Items (4)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Real-time logics: Complexity and expressiveness
- The complexity of membership problems for circuits over sets of integers
- Model checking memoryful linear-time logics over one-counter automata
- An until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic
- Uniform constant-depth threshold circuits for division and iterated multiplication.
- LTL with the freeze quantifier and register automata
- Path Checking for MTL and TPTL over Data Words
- Model Checking One-clock Priced Timed Automata
- A really temporal logic
- Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds
- Model Checking Metric Temporal Logic over Automata with One Counter
- On the Complexity of Temporal-Logic Path Checking
- On the decidability and complexity of Metric Temporal Logic over finite words
- Satisfiability for MTL and TPTL over Non-monotonic Data Words
- Foundations of Software Science and Computation Structures
This page was built for publication: Path Checking for MTL and TPTL over Data Words
