A Dose of Timed Logic, in Guarded Measure

We consider interval measurement logic IML, a sublogic of Zhou and Hansen's interval logic, with measurement functions which provide real-valued measurement of some aspect of system behaviour in a given time interval. We interpret IML over a variety of time domains (continuous, sampled, integer) and show that it can provide a unified treatment of many diverse temporal logics including duration calculus (DC), interval duration logic (IDL) and metric temporal logic (MTL). We introduce a fragment GIML with restricted measurement modalities which subsumes most of the decidable timed logics considered in the literature. Next, we introduce a guarded first-order logic with measurements MGF. As a generalisation of Kamp's theorem, we show that over arbitrary time domains, the measurement logic GIML is expressively complete for it. We also show that MGF has the 3-variable property. In addition, we have a preliminary result showing the decidability of a subset of GIML when interpreted o...

• Type: Conference
• Year: 2006
• Where: FORMATS
• Authors: Kamal Lodaya, Paritosh K. Pandya
• Keywords: Formal Methods, FORMATS 2006, Logic, Measurement, Measurement Functions