### Resumé

The method is based on the existence of a quotient construction, allowing a property phi of a parallel system phi/A to be transformed into a sufficient and necessary quotient-property yolA to be satisfied by the component 13. Given a model checking problem involving a network Pi I and a property yo, the method gradually move (by quotienting) components Pi from the network into the formula co. Crucial to the success of the method is the ability to manage the size of the intermediate quotient-properties by a suitable collection of efficient minimization heuristics.

Originalsprog | Engelsk |
---|---|

Bogserie | Lecture Notes in Computer Science |

Udgave nummer | 5947 |

Sider (fra-til) | 35-42 |

Antal sider | 7 |

ISSN | 0302-9743 |

Status | Udgivet - 2010 |

### Bibliografisk note

ISBN: 978-3-642-11485-4### Citer dette

*Lecture Notes in Computer Science*, ( 5947), 35-42.

}

*Lecture Notes in Computer Science*, nr. 5947, s. 35-42.

**Compositional and Quantitative Model Checking.** / Larsen, Kim Guldstrand.

Publikation: Bidrag til tidsskrift › Konferenceartikel i tidsskrift › Forskning › peer review

TY - GEN

T1 - Compositional and Quantitative Model Checking

AU - Larsen, Kim Guldstrand

N1 - ISBN: 978-3-642-11485-4

PY - 2010

Y1 - 2010

N2 - This paper gives a survey of a composition model checking methodology and its succesfull instantiation to the model checking of networks of finite-state, timed, hybrid and probabilistic systems with respect; to suitable quantitative versions of the modal mu-calculus [Koz82]. The method is based on the existence of a quotient construction, allowing a property phi of a parallel system phi/A to be transformed into a sufficient and necessary quotient-property yolA to be satisfied by the component 13. Given a model checking problem involving a network Pi I and a property yo, the method gradually move (by quotienting) components Pi from the network into the formula co. Crucial to the success of the method is the ability to manage the size of the intermediate quotient-properties by a suitable collection of efficient minimization heuristics.

AB - This paper gives a survey of a composition model checking methodology and its succesfull instantiation to the model checking of networks of finite-state, timed, hybrid and probabilistic systems with respect; to suitable quantitative versions of the modal mu-calculus [Koz82]. The method is based on the existence of a quotient construction, allowing a property phi of a parallel system phi/A to be transformed into a sufficient and necessary quotient-property yolA to be satisfied by the component 13. Given a model checking problem involving a network Pi I and a property yo, the method gradually move (by quotienting) components Pi from the network into the formula co. Crucial to the success of the method is the ability to manage the size of the intermediate quotient-properties by a suitable collection of efficient minimization heuristics.

M3 - Conference article in Journal

SP - 35

EP - 42

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

IS - 5947

ER -