|   | 
Details
   web
Records
Author (up) Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry
Title Model Checking Nash Equilibria in MAD Distributed Systems Type Conference Article
Year 2008 Publication FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design Abbreviated Journal
Volume Issue Pages 1-8
Keywords Model Checking, MAD Distributed System, Nash Equilibrium
Abstract We present a symbolic model checking algorithm for verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems. Given a finite state mechanism, a proposed protocol for each agent and an indifference threshold for rewards, our model checker returns PASS if the proposed protocol is a Nash equilibrium (up to the given indifference threshold) for the given mechanism, FAIL otherwise. We implemented our model checking algorithm inside the NuSMV model checker and present experimental results showing its effectiveness for moderate size mechanisms. For example, we can handle mechanisms which corresponding normal form games would have more than $10^20$ entries. To the best of our knowledge, no model checking algorithm for verification of mechanism Nash equilibria has been previously published.
Address
Corporate Author Thesis
Publisher IEEE Press Place of Publication Piscataway, NJ, USA Editor Cimatti, A.; Jones, R.
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 978-1-4244-2735-2 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ MarMelSalTroAlvCle08 Serial 93
Permanent link to this record
 

 
Author (up) Mari, Federico; Melatti, Igor; Tronci, Enrico; Finzi, Alberto
Title A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET Type Journal Article
Year 2013 Publication Mobile Information Systems Abbreviated Journal Mobile Information Systems
Volume 3 Issue 9 Pages 261-280
Keywords
Abstract
Address
Corporate Author Thesis
Publisher IOS Press Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 1574-017x (Print) 1875-905X (Online) ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ melatti @ Serial 109
Permanent link to this record
 

 
Author (up) Mari, Federico; Tronci, Enrico
Title CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems Type Conference Article
Year 2007 Publication Hybrid Systems: Computation and Control (HSCC 2007) Abbreviated Journal
Volume Issue Pages 399-412
Keywords Model Checking, Abstraction, CEGAR, SAT, Hybrid Systems, DTHS
Abstract Many hybrid systems can be conveniently modeled as Piecewise Affine Discrete Time Hybrid Systems PA-DTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem. We present a SAT based BMC algorithm for automatic verification of PA-DTHSs. Using Counterexample Guided Abstraction Refinement (CEGAR) our algorithm gradually transforms a PA-DTHS verification problem into larger and larger SAT problems. Our experimental results show that our approach can handle PA-DTHSs that are more then 50 times larger than those that can be handled using a MILP solver.
Address
Corporate Author Thesis
Publisher Springer Place of Publication Editor Bemporad, A.; Bicchi, A.; Buttazzo, G.C.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 4416 Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ MarTro07 Serial 92
Permanent link to this record
 

 
Author (up) Mazzini, Silvia; Puri, Stefano; Mari, Federico; Melatti, Igor; Tronci, Enrico
Title Formal Verification at System Level Type Conference Article
Year 2009 Publication In: DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. Instanbul, Turkey, EuroSpace Abbreviated Journal
Volume Issue Pages
Keywords
Abstract System Level Analysis calls for a language comprehensible to experts with different background and yet precise enough to support meaningful analyses. SysML is emerging as an effective balance between such conflicting goals. In this paper we outline some the results obtained as for SysML based system level functional formal verification by an ESA/ESTEC study, with a collaboration among INTECS and La Sapienza University of Roma. The study focuses on SysML based system level functional requirements techniques.
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dasia09 Serial 20
Permanent link to this record
 

 
Author (up) Melatti, I.; Mari, F.; Mancini, T.; Prodanovic, M.; Tronci, E.
Title A Two-Layer Near-Optimal Strategy for Substation Constraint Management via Home Batteries Type Journal Article
Year 2021 Publication IEEE Transactions on Industrial Electronics Abbreviated Journal
Volume Issue Pages 1-1
Keywords
Abstract Within electrical distribution networks, substation constraints management requires that aggregated power demand from residential users is kept within suitable bounds. Efficiency of substation constraints management can be measured as the reduction of constraints violations w.r.t. unmanaged demand. Home batteries hold the promise of enabling efficient and user-oblivious substation constraints management. Centralized control of home batteries would achieve optimal efficiency. However, it is hardly acceptable by users, since service providers (e.g., utilities or aggregators) would directly control batteries at user premises. Unfortunately, devising efficient hierarchical control strategies, thus overcoming the above problem, is far from easy. We present a novel two-layer control strategy for home batteries that avoids direct control of home devices by the service provider and at the same time yields near-optimal substation constraints management efficiency. Our simulation results on field data from 62 households in Denmark show that the substation constraints management efficiency achieved with our approach is at least 82% of the one obtained with a theoretical optimal centralized strategy.
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes To appear Approved no
Call Number MCLab @ davi @ ref9513535 Serial 190
Permanent link to this record
 

 
Author (up) Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.; Mari, F.; Leeners, B.
Title Optimal Personalised Treatment Computation through In Silico Clinical Trials on Patient Digital Twins Type Journal Article
Year 2020 Publication Abbreviated Journal Fundamenta Informaticae
Volume 174 Issue Pages 283-310
Keywords Artificial Intelligence; Virtual Physiological Human; In Silico Clinical Trials; Simulation; Personalised Medicine; In Silico Treatment Optimisation
Abstract In Silico Clinical Trials (ISCT), i.e. clinical experimental campaigns carried out by means of computer simulations, hold the promise to decrease time and cost for the safety and efficacy assessment of pharmacological treatments, reduce the need for animal and human testing, and enable precision medicine. In this paper we present methods and an algorithm that, by means of extensive computer simulation-based experimental campaigns (ISCT) guided by intelligent search, optimise a pharmacological treatment for an individual patient (precision medicine ). We show the effectiveness of our approach on a case study involving a real pharmacological treatment, namely the downregulation phase of a complex clinical protocol for assisted reproduction in humans.
Address
Corporate Author Thesis
Publisher IOS Press Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 1875-8681 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Serial 187
Permanent link to this record
 

 
Author (up) Toni Mancini; Enrico Tronci; Ivano Salvo; Federico Mari; Annalisa Massini; Igor Melatti
Title Computing Biological Model Parameters by Parallel Statistical Model Checking Type Journal Article
Year 2015 Publication International Work Conference on Bioinformatics and Biomedical Engineering (IWBBIO 2015) Abbreviated Journal
Volume 9044 Issue Pages 542-554
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Serial 124
Permanent link to this record
 

 
Author (up) Tronci, E.; Mancini, T.; Mari, F.; Melatti, I.; Jacobsen, R. H.; Ebeid, E.; Mikkelsen, S. A.; Prodanovic, M.; Gruber, J. K.; Hayes, B.
Title SmartHG: Energy Demand Aware Open Services for Smart Grid Intelligent Automation Type Conference Article
Year 2014 Publication Proceedings of the Work in Progress Session of SEAA/DSD 2014 Abbreviated Journal
Volume Issue Pages
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN 978-3-902457-40-0 Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ mari @ Serial 119
Permanent link to this record
 

 
Author (up) Tronci, E.; Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Prodanovic, M.; Gruber, J. K.; Hayes, B.; Elmegaard, L.
Title Demand-Aware Price Policy Synthesis and Verification Services for Smart Grids Type Conference Article
Year 2014 Publication Proceedings of Smart Grid Communications (SmartGridComm), 2014 IEEE International Conference On Abbreviated Journal
Volume Issue Pages
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ melatti @ Serial 121
Permanent link to this record
 

 
Author (up) Tronci, E.; Mancini, T.; Salvo, I.; Mari, F.; Melatti, I.; Massini, A.; Sinisi, S.; Davì, F.; Dierkes, T.; Ehrig, R.; Röblitz, S.; Leeners, B.; Krüger, T.; Egli, M.; Ille, F.
Title Patient-Specific Models from Inter-Patient Biological Models and Clinical Records Type Conference Article
Year 2014 Publication Formal Methods in Computer-Aided Design (FMCAD) Abbreviated Journal
Volume Issue Pages
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ mari @ Serial 120
Permanent link to this record