Sebastian, Preugschat and Wilke, Thomas - Effective Characterizations of Simple Fragments of Temporal Logic Using Carton--Michel Automata

lmcs:909 - Logical Methods in Computer Science, June 21, 2013, Volume 9, Issue 2
Effective Characterizations of Simple Fragments of Temporal Logic Using Carton--Michel Automata

Authors: Sebastian, Preugschat and Wilke, Thomas

We present a framework for obtaining effective characterizations of simple fragments of future temporal logic (LTL) with the natural numbers as time domain. The framework is based on a form of strongly unambiguous automata, also known as prophetic automata or complete unambiguous B\"uchi automata and referred to as Carton-Michel automata in this paper. These automata enjoy strong structural properties, in particular, they separate the "finitary fraction" of a regular language of infinite words from its "infinitary fraction" in a natural fashion. Within our framework, we provide characterizations of several natural fragments of temporal logic, where, in some cases, no effective characterization had been known previously, and give lower and upper bounds for their computational complexity.


Source : oai:arXiv.org:1303.5956
DOI : 10.2168/LMCS-9(2:8)2013
Volume: Volume 9, Issue 2
Published on: June 21, 2013
Submitted on: August 31, 2012
Keywords: Computer Science - Formal Languages and Automata Theory,Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 66 times.
This article's PDF has been downloaded 91 times.