CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Bounded variability of metric temporal logic

Carlo A. Furia (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; P. Spoletini
Annals of Mathematics and Artificial Intelligence (1012-2443). Vol. 80 (2017), 3-4, p. 283-316.
[Artikel, refereegranskad vetenskaplig]

Deciding validity of Metric Temporal Logic (MTL) formulas is generally very complex and even undecidable over dense time domains; bounded variability is one of the several restrictions that have been proposed to bring decidability back. A temporal model has bounded variability if no more than v events occur over any time interval of length V, for constant parameters v and V. Previous work has shown that MTL validity over models with bounded variability is less complex—and often decidable—than MTL validity over unconstrained models. This paper studies the related problem of deciding whether an MTL formula has intrinsic bounded variability, that is whether it is satisfied only by models with bounded variability. The results of the paper are mainly negative: over dense time domains, the problem is mostly undecidable (even if with an undecidability degree that is typically lower than deciding validity); over discrete time domains, it is decidable with the same complexity as deciding validity. As a partial complement to these negative results, the paper also identifies MTL fragments where deciding bounded variability is simpler than validity, which may provide for a reduction in complexity in some practical cases.

Nyckelord: Bounded variability, Decidability and complexity, Metric temporal logic



Denna post skapades 2017-01-16. Senast ändrad 2017-08-10.
CPL Pubid: 247116

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)

Ämnesområden

Datalogi

Chalmers infrastruktur