A formal and run-time framework for the adaptation of local behaviours to match a global property

A formal and run-time framework for the adaptation of local behaviours to match a global property. Bistarelli, S., Martinelli, F., Matteucci, I., & Santini, F. 2017.

Paper doi abstract bibtex

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 φ. 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 φ. The proposed approach can be seen as a run-time decomposition, privacysensitive in the sense agents do not have to disclose their full behaviour.

@conference{
	11391_1409310,
	author = {Bistarelli, Stefano and Martinelli, Fabio and Matteucci, Ilaria and Santini, Francesco},
	title = {A formal and run-time framework for the adaptation of local behaviours to match a global property},
	year = {2017},
	publisher = {Springer Verlag},
	volume = {10231},
	booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
	abstract = {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 φ. 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 φ. The proposed approach can be seen as a run-time decomposition, privacysensitive in the sense agents do not have to disclose their full behaviour.},
	keywords = {Computer software; Embedded systems; Machinery; Model checking, Local property; Modal logic; Partial model checking; Runtimes},
	url = {http://springerlink.com/content/0302-9743/copyright/2005/},
	doi = {10.1007/978-3-319-57666-4_9},	
	pages = {134--152}
}

Downloads: 0

{"_id":"ajwJvsKxwyLKwG5WZ","bibbaseid":"bistarelli-martinelli-matteucci-santini-aformalandruntimeframeworkfortheadaptationoflocalbehaviourstomatchaglobalproperty-2017","author_short":["Bistarelli, S.","Martinelli, F.","Matteucci, I.","Santini, F."],"bibdata":{"bibtype":"conference","type":"conference","author":[{"propositions":[],"lastnames":["Bistarelli"],"firstnames":["Stefano"],"suffixes":[]},{"propositions":[],"lastnames":["Martinelli"],"firstnames":["Fabio"],"suffixes":[]},{"propositions":[],"lastnames":["Matteucci"],"firstnames":["Ilaria"],"suffixes":[]},{"propositions":[],"lastnames":["Santini"],"firstnames":["Francesco"],"suffixes":[]}],"title":"A formal and run-time framework for the adaptation of local behaviours to match a global property","year":"2017","publisher":"Springer Verlag","volume":"10231","booktitle":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","abstract":"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 φ. 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 φ. The proposed approach can be seen as a run-time decomposition, privacysensitive in the sense agents do not have to disclose their full behaviour.","keywords":"Computer software; Embedded systems; Machinery; Model checking, Local property; Modal logic; Partial model checking; Runtimes","url":"http://springerlink.com/content/0302-9743/copyright/2005/","doi":"10.1007/978-3-319-57666-4_9","pages":"134–152","bibtex":"@conference{\n\t11391_1409310,\n\tauthor = {Bistarelli, Stefano and Martinelli, Fabio and Matteucci, Ilaria and Santini, Francesco},\n\ttitle = {A formal and run-time framework for the adaptation of local behaviours to match a global property},\n\tyear = {2017},\n\tpublisher = {Springer Verlag},\n\tvolume = {10231},\n\tbooktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},\n\tabstract = {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 φ. 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 φ. The proposed approach can be seen as a run-time decomposition, privacysensitive in the sense agents do not have to disclose their full behaviour.},\n\tkeywords = {Computer software; Embedded systems; Machinery; Model checking, Local property; Modal logic; Partial model checking; Runtimes},\n\turl = {http://springerlink.com/content/0302-9743/copyright/2005/},\n\tdoi = {10.1007/978-3-319-57666-4_9},\t\n\tpages = {134--152}\n}\n","author_short":["Bistarelli, S.","Martinelli, F.","Matteucci, I.","Santini, F."],"key":"11391_1409310","id":"11391_1409310","bibbaseid":"bistarelli-martinelli-matteucci-santini-aformalandruntimeframeworkfortheadaptationoflocalbehaviourstomatchaglobalproperty-2017","role":"author","urls":{"Paper":"http://springerlink.com/content/0302-9743/copyright/2005/"},"keyword":["Computer software; Embedded systems; Machinery; Model checking","Local property; Modal logic; Partial model checking; Runtimes"],"metadata":{"authorlinks":{}},"downloads":0,"html":""},"bibtype":"conference","biburl":"http://www.dmi.unipg.it/~bista/papers/pubblicazioni.bib","dataSources":["GhB5rb8JzW6az3exo"],"keywords":["computer software; embedded systems; machinery; model checking","local property; modal logic; partial model checking; runtimes"],"search_terms":["formal","run","time","framework","adaptation","local","behaviours","match","global","property","bistarelli","martinelli","matteucci","santini"],"title":"A formal and run-time framework for the adaptation of local behaviours to match a global property","year":2017}