Keywords:
Forschungsbericht
Description / Table of Contents:
In this paper, we describe the design and implementation of (several variants of) a local parallel model checking algorithm for the alternation free fragment of the mu-calculus. It exploits a characterisation of the model checking problem for this fragment in terms of two-player games. Our algorithm determines the corresponding winner in parallel. Furthermore, a winning strategy is computed which may be employed for interactively debugging the underlying system. The algorithm is designed to run on a network of workstations. Depending on the chosen variant, its complexity is linear or quadratic. A prototype implementation within the verification tool Truth shows promising run--time and memory behaviour in practice.
Type of Medium:
Online Resource
Pages:
Online-Ressource (38 S., 617 KB)
,
graph. Darst.
Series Statement:
Aachener Informatik-Berichte 2001, 04
URL:
http://webdoc.sub.gwdg.de/ebook/serien/ah/AIB/2001-04.ps
URL:
https://edocs.tib.eu/files/e01fn09/501003037.pdf
URL:
https://edocs.tib.eu/files/e01fn09/501003037l.pdf
Language:
English
Note:
Unterschiede zwischen dem gedruckten Dokument und der elektronischen Ressource können nicht ausgeschlossen werden. - Auch als gedr. Ausg. vorhanden
,
Systemvoraussetzungen: Acrobat reader.
Permalink