Witness and counterexample automata for ACTL (Articolo in rivista)

Type
Label
  • Witness and counterexample automata for ACTL (Articolo in rivista) (literal)
Anno
  • 2004-01-01T00:00:00+01:00 (literal)
Alternative label
  • Meolic R.; Fantechi A.; Gnesi S. (2004)
    Witness and counterexample automata for ACTL
    in Lecture notes in computer science
    (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
  • Meolic R.; Fantechi A.; Gnesi S. (literal)
Pagina inizio
  • 259 (literal)
Pagina fine
  • 275 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#numeroVolume
  • 3235 (literal)
Rivista
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#note
  • FORTE 2004: 24th IFIP WG 6.1 International Conference (Madrid, Spain, September 27-30, 2004). David de Frutos-Escrig, Manuel Nunez (Eds.). Proceedings, Springer, 2004. (literal)
Note
  • Scopu (literal)
  • ISI Web of Science (WOS) (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni
  • University of Maribor, Slovenia Università di Firenze, Italia, ISTI-CNR, Italia (literal)
Titolo
  • Witness and counterexample automata for ACTL (literal)
Abstract
  • Witnesses and counterexamples produced by model checkers provide a very useful source of diagnostic information. They are usually returned in the form of a single computation path along the model of the system. However, a single computation path is not enough to explain all reasons of a validity or a failure. Our work in this area is motivated by the application of action-based model checking algorithms to the test case generation for models formally specified with a CCS-like process algebra. There, only linear and finite witnesses and counterexamples are useful and for the given formula and model an efficient representation of the set of witnesses (counterexamples) explaining all reasons of validity (failure) is needed. This paper identifies a fragment of action computation tree logic (ACTL) that can be handled in this way. Moreover, a suitable form of witnesses and counterexamples is proposed and witness and counterexample automata are introduced, which are finite automata recognizing them. An algorithm for generating such automata is given. (literal)
Prodotto di
Autore CNR

Incoming links:


Prodotto
Autore CNR di
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#rivistaDi
data.CNR.it