Advertisement
Published in:
2010 | OriginalPaper | Chapter
Kleene, Rabin, and Scott Are Available
Authors : Jochen Hoenicke, Roland Meyer, Ernst-Rüdiger Olderog
Published in: CONCUR 2010 - Concurrency Theory
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We are concerned with the availability of systems, defined as the ratio between time of correct functioning and uptime. We propose to model guaranteed availability in terms of
regular availability expressions
(rae) and
availability automata
. We prove that the intersection problem of rae is undecidable. We establish a Kleene theorem that shows the equivalence of the formalisms and states precise correspondence of flat rae and simple availability automata. For these automata, we provide an extension of the powerset construction for finite automata due to Rabin and Scott. As a consequence, we can state a complementation algorithm. This enables us to solve the synthesis problem and to reduce model checking of availability properties to reachability.