Interval Duration Logic: Expressiveness and Decidability

9 years 3 months ago
Interval Duration Logic: Expressiveness and Decidability
We investigate a variant of dense-time Duration Calculus which permits model checking using timed/hybrid automata. We define a variant of the Duration Calculus, called Interval Duration Logic, (IDL), whose models are timed state sequences [1]. A subset LIDL of IDL consisting only of located time constraints is presented. As our main result, we show that the models of an LIDL formula can be captured as timed state sequences accepted by an event-recording integrator automaton. A tool called IDLVALID for reducing LIDL formulae to integrator automata is briefly described. Finally, it is shown that LIDL has precisely the expressive power of event-recording integrator automata, and that a further subset LIDL- corresponds exactly to event-recording timed automata [2]. This gives us an automata-theoretic decision procedure for the satisfiability of LIDL- formulae.
Paritosh K. Pandya
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2002
Authors Paritosh K. Pandya
Comments (0)