A model has variability bounded by v/k when the state changes at most v times over any linear interval containing k time instants. When interpreted over models with bounded variability, specification formulae that contain redundant metric information---through the usage of next operators---can be simplified without affecting their validity. This paper shows how to harness this simplification in practice: we present a translation of LTL into Büchi automata that removes redundant metric information, hence makes for more efficient verification over models with bounded variability. To show the feasibility of the approach, we also implement a proof-of-concept translation in ProMeLa and verify it using the Spin off-the-shelf model-checker.

Automata-based Verification of Linear Temporal Logic Models with Bounded Variability

SPOLETINI, PAOLA
2012

Abstract

A model has variability bounded by v/k when the state changes at most v times over any linear interval containing k time instants. When interpreted over models with bounded variability, specification formulae that contain redundant metric information---through the usage of next operators---can be simplified without affecting their validity. This paper shows how to harness this simplification in practice: we present a translation of LTL into Büchi automata that removes redundant metric information, hence makes for more efficient verification over models with bounded variability. To show the feasibility of the approach, we also implement a proof-of-concept translation in ProMeLa and verify it using the Spin off-the-shelf model-checker.
9781467326599
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11383/1792042
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact