On-the-fly automata construction for dynamic linear time temporal logic

Laura Giordano; Alberto Martelli

doi:10.1109/time.2004.1314430

On-the-fly automata construction for dynamic linear time temporal logic

Laura Giordano, Alberto Martelli

Dipartimento di Scienze e Innovazione Tecnologica

Risultato della ricerca: Contributo alla conferenza › Contributo in Atti di Convegno › peer review

Abstract

We present a tableau-based algorithm for obtaining a Büchi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Büchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton.

Lingua originale	Inglese
Pagine	133-139
Numero di pagine	7
DOI	https://doi.org/10.1109/time.2004.1314430
Stato di pubblicazione	Pubblicato - 2004
Evento	Proceedings - 11th International Symposium on Temporal Representation and Reasoning (TIME 2004) - Tatihou, France Durata: 1 lug 2004 → 3 lug 2004

???event.eventtypes.event.conference???

???event.eventtypes.event.conference???	Proceedings - 11th International Symposium on Temporal Representation and Reasoning (TIME 2004)
Paese/Territorio	France
Città	Tatihou
Periodo	1/07/04 → 3/07/04

Accesso al documento

10.1109/time.2004.1314430

Altri file e collegamenti

Link to publication in Scopus

Cita questo

@conference{80ac6e81236644c8a4ff7428d3ef2afe,

title = "On-the-fly automata construction for dynamic linear time temporal logic",

abstract = "We present a tableau-based algorithm for obtaining a B{\"u}chi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a B{\"u}chi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton.",

author = "Laura Giordano and Alberto Martelli",

year = "2004",

doi = "10.1109/time.2004.1314430",

language = "English",

pages = "133--139",

note = "Proceedings - 11th International Symposium on Temporal Representation and Reasoning (TIME 2004) ; Conference date: 01-07-2004 Through 03-07-2004",

}

TY - CONF

T1 - On-the-fly automata construction for dynamic linear time temporal logic

AU - Giordano, Laura

AU - Martelli, Alberto

PY - 2004

Y1 - 2004

N2 - We present a tableau-based algorithm for obtaining a Büchi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Büchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton.

AB - We present a tableau-based algorithm for obtaining a Büchi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Büchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton.

UR - http://www.scopus.com/inward/record.url?scp=5644243255&partnerID=8YFLogxK

U2 - 10.1109/time.2004.1314430

DO - 10.1109/time.2004.1314430

M3 - Paper

SP - 133

EP - 139

T2 - Proceedings - 11th International Symposium on Temporal Representation and Reasoning (TIME 2004)

Y2 - 1 July 2004 through 3 July 2004

ER -

On-the-fly automata construction for dynamic linear time temporal logic

Abstract

???event.eventtypes.event.conference???

Accesso al documento

Altri file e collegamenti

Fingerprint

Cita questo