Zur Seitenansicht
 

Titelaufnahme

Titel
Model Checking Parameterised Multi-token Systems via the Composition Method
Verfasser / Verfasserin Aminof, Benjamin ; Rubin, Sasha
Erschienen in
Automated Reasoning. 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 July 2, 2016, Proceedings : Olivetti, Nicola; Tiwari, Ashish, Portugal, 2016, S. 499-515
Erschienen2016
SpracheEnglisch
SerieLecture Notes in Artificial Intelligence ; 9706
DokumenttypAufsatz in einem Sammelwerk
Projekt-/ReportnummerVienna Science Fund (WWTF): ICT12-059
ISBN9783319402291
URNurn:nbn:at:at-ubtuw:3-3798 Persistent Identifier (URN)
DOI10.1007/978-3-319-40229-1_34 
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Model Checking Parameterised Multi-token Systems via the Composition Method [0.51 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Englisch)

We study the model checking problem of parameterised systems with an arbitrary number of processes, on arbitrary network-graphs, communicating using multiple multi-valued tokens, and specifications from indexed-branching temporal logic. We prove a composition theorem, in the spirit of Feferman-Vaught [21] and Shelah [31], and a finiteness theorem, and use these to decide the model checking problem. Our results assume two constraints on the process templates, one of which is the standard fairness assumption introduced in the cornerstone paper of Emerson and Namjoshi [18]. We prove that lifting any of these constraints results in undecidability. The importance of our work is three-fold: (i) it demonstrates that the composition method can be fruitfully applied to model checking complex parameterised systems; (ii) it identifies the most powerful model, to date, of parameterised systems for which model checking indexed branching-time specifications is decidable; (iii) it tightly marks the borders of decidability of this model.

Notiz
Notiz
Statistik
Das PDF-Dokument wurde 9 mal heruntergeladen.