We study model-checking problems on counter systems when guards are quantifier-free Presburger formulae, the specification languages are LTL-like dialects with arithmetical constraints and the runs are restricted to reversal-bounded ones. We introduce a generalization of reversal-boundedness and we show the NExpTime-completeness of the reversal-bounded model-checking problem as well as for related reversalbounded reachability problems. As a by-product, we show the effective Presburger definability for sets of configurations for which there is a reversal-bounded run verifying a given temporal formula. Our results generalize existing results about reversal-bounded counter automata and provides a uniform and more general framework.

The Complexity of Reversal-Bounded Model-Checking.

BERSANI, MARCELLO MARIA;
2011-01-01

Abstract

We study model-checking problems on counter systems when guards are quantifier-free Presburger formulae, the specification languages are LTL-like dialects with arithmetical constraints and the runs are restricted to reversal-bounded ones. We introduce a generalization of reversal-boundedness and we show the NExpTime-completeness of the reversal-bounded model-checking problem as well as for related reversalbounded reachability problems. As a by-product, we show the effective Presburger definability for sets of configurations for which there is a reversal-bounded run verifying a given temporal formula. Our results generalize existing results about reversal-bounded counter automata and provides a uniform and more general framework.
Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrucken, Germany, October 5-7, 2011. Proceedings
9783642243639
File in questo prodotto:
File Dimensione Formato  
frocos2011.pdf

Accesso riservato

Dimensione 287.06 kB
Formato Adobe PDF
287.06 kB Adobe PDF   Visualizza/Apri

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: https://hdl.handle.net/11311/635444
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact