|
|
|
                                          
|
Return to Research Papers
We present a tableau-based algorithm for obtaining a Bšuchi 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šuchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton.
@inproceedings{DBLP:conf/time/GiordanoM04, author = {Laura Giordano and Alberto Martelli}, title = {On-the-Fly Automata Construction for Dynamic Linear Time Temporal Logic.}, booktitle = {TIME}, year = {2004}, pages = {133-139}, ee = {http://csdl.computer.org/comp/proceedings/time/2004/2155/00/21550133abs.htm}, crossref = {conf/time/2004}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/time/2004, title = {11th International Symposium on Temporal Representation and Reasoning (TIME 2004), 1-3 July 2004, Tatihou Island, Normandie, France}, booktitle = {TIME}, publisher = {IEEE Computer Society}, year = {2004}, isbn = {0-7695-2155-X}, bibsource = {DBLP, http://dblp.uni-trier.de} } },  ©2005 Association for Computing Machinery |
