Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-15375-4_32 | CONCUR |
Keywords | Field | DocType |
complementation algorithm,model checking,intersection problem,simple availability automaton,regular availability expression,kleene theorem,flat rae,synthesis problem,availability property,availability automaton,finite automata | Quantum finite automata,Discrete mathematics,Model checking,Expression (mathematics),Computer science,Automaton,Finite-state machine,Reachability,Equivalence (measure theory),Undecidable problem | Conference |
Volume | ISSN | ISBN |
6269 | 0302-9743 | 3-642-15374-7 |
Citations | PageRank | References |
4 | 0.43 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jochen Hoenicke | 1 | 292 | 20.43 |
| Roland Meyer | 2 | 203 | 15.99 |
| Ernst-Rüdiger Olderog | 3 | 682 | 220.84 |