School of Computing

From LIDL(m) to Timed Automata

Rodolfo Gomez

Technical Report TR-2-09-2009, Computing Laboratory, University of Kent, April 2009.

Abstract

LIDL(m) is a decidable fragment of Interval Duration Logic with Located Constraints, an expressive subset of dense-time Duration Calculus. It has been claimed that, for any LIDL(m) formula D, a timed automaton can be constructed which accepts the models of D. However, the proposed construction is incomplete and has not been proved effective. In this paper, we prove the effective construction of equivalent timed automata from LIDL(m) formulae.

Download publication 214 kbytes (PDF)

Bibtex Record

@techreport{2890,
author = {Rodolfo Gomez},
title = {From {LIDL}(m)  to {T}imed {A}utomata},
month = {April},
year = {2009},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2009/2890},
    publication_type = {techreport},
    submission_id = {27497_1238600841},
    institution = {Computing Laboratory, University of Kent},
    number = {TR-2-09-2009},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014