Büchi-Kamp Theorems for 1-clock ATA

2018/02/06 by Shankara Narayanan Krishna, Krishna, Shankara Narayanan, Khushraj Madnani +3
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO

paper · pdf · doi:10.48550/arxiv.1802.02514

arxiv created 2018/02/06 · arxiv updated 2018/02/08

Abstract

This paper investigates Kamp-like and Büchi-like theorems for 1-clock Alternating Timed Automata (1-ATA) and its natural subclasses. A notion of 1-ATA with loop-free-resets is defined. This automaton class is shown to be expressively equivalent to the temporal logic \regmtl which is MTL[F_I] extended with a regular expression guarded modality. Moreover, a subclass of future timed MSO with k-variable-connectivity property is introduced as logic \qkmso. In a Kamp-like result, it is shown that \regmtl is expressively equivalent to \qkmso. As our second result, we define a notion of conjunctive-disjunctive 1-clock ATA (\wf 1-ATA). We show that \wf 1-ATA with loop-free-resets are expressively equivalent to the sublogic \F\regmtl of \regmtl. Moreover \F\regmtl is expressively equivalent to \qtwomso, the two-variable connected fragment of \qkmso. The full class of 1-ATA is shown to be expressively equivalent to \regmtl extended with fixed point operators.

Related

• Logics Meet 2-Way 1-Clock Alternating Timed Automata
• A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata
• On MITL and alternating timed automata
• Making Metric Temporal Logic Rational
• Model-checking real-time systems: revisiting the alternating automaton route