Frequency Linear-time Temporal Logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

Frequency Linear-time Temporal Logic

Résumé

We propose fLTL, an extension to linear-time temporal logic (LTL) that allows for expressing relative frequencies by a generalization of temporal operators. This facilitates the specification of requirements such as the deadlines in a real-time system must be met in at least 95% of all cases. For our novel logic, we establish an undecidability result regarding the satisfiability problem but identify a decidable fragment which strictly increases the expressiveness of LTL by allowing, e.g., to express non-context-free properties.

Domaines

Autre [cs.OH]

Dates et versions

hal-00776769 , version 1 (16-01-2013)

Identifiants

Citer

Benedikt Bollig, Normann Decker, Martin Leucker. Frequency Linear-time Temporal Logic. Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12), 2012, Beijing, China. pp.85-92, ⟨10.1109/TASE.2012.43⟩. ⟨hal-00776769⟩
82 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More