A Formal and Run-Time Framework for the Adaptation of Local Behaviours to Match a Global Property
| Autor: | Ilaria Matteucci, Francesco Santini, Stefano Bistarelli, Fabio Martinelli |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Model checking
Knowledge management Property (philosophy) Theoretical computer science Computer science Embedded systems media_common.quotation_subject 0102 computer and information sciences 02 engineering and technology 01 natural sciences Machinery Runtimes 0202 electrical engineering electronic engineering information engineering Decomposition (computer science) Computer software Function (engineering) Adaptation (computer science) Partial model checking media_common Model checking Local property Modal logic business.industry Cyber-physical systems Cyber-physical system Required property 010201 computation theory & mathematics Model-based adaptation Local property 020201 artificial intelligence & image processing business |
| Zdroj: | Formal Aspects of Component Software ISBN: 9783319576657 FACS BASE-Bielefeld Academic Search Engine Formal Aspects of Component Software-13th International Conference, FACS 2016, Besançon, France, October 19-21, 2016, Revised Selected Papers Lecture Notes in Computer Science Lecture Notes in Computer Science-Formal Aspects of Component Software Formal Aspects of Component Software-The 13th International Conference, Besançon, France, 19/10/2016 info:cnr-pdr/source/autori:F. Martinelli(1), I. Matteucci(1), S. Bistarelli(2), F. Santini(2)/congresso_nome:Formal Aspects of Component Software-The 13th International Conference/congresso_luogo:Besançon, France/congresso_data:19%2F10%2F2016/anno:2016/pagina_da:/pagina_a:/intervallo_pagine |
| ISSN: | 0302-9743 1611-3349 |
| DOI: | 10.1007/978-3-319-57666-4_9 |
| Popis: | We address the problem of automatically identifying what local properties the agents of a Cyber Physical System have to satisfy to guarantee a global required property \(\phi \). To enrich the picture, we consider properties where, besides qualitative requirements on the actions to be performed, we assume a weight associated with them: quantitative properties are specified through a weighted modal-logic. We propose both a formal machinery based on a Quantitative Partial Model Checking function on contexts, and a run-time machinery that algorithmically tries to check if the local behaviours proposed by the agents satisfy \(\phi \). The proposed approach can be seen as a run-time decomposition, privacy-sensitive in the sense agents do not have to disclose their full behaviour. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|