| Records |
| Author |
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 |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry |
| Title |
Model Checking Coalition Nash Equilibria in MAD Distributed Systems |
Type |
Conference Article |
| Year |
2009 |
Publication |
Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, SSS 2009, Lyon, France, November 3-6, 2009. Proceedings |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
531-546 |
| Keywords |
|
| Abstract |
We present two OBDD based model checking algorithms for the verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems with possibly colluding agents (coalitions) and with possibly faulty or malicious nodes (Byzantine agents). Given a finite state mechanism, a proposed protocol for each agent and the maximum sizes f for Byzantine agents and q for agents collusions, our model checkers return Pass if the proposed protocol is an ε-f-q-Nash equilibrium, i.e. no coalition of size up to q may have an interest greater than ε in deviating from the proposed protocol when up to f Byzantine agents are present, Fail otherwise. We implemented our model checking algorithms within the NuSMV model checker: the first one explicitly checks equilibria for each coalition, while the second represents symbolically all coalitions. We present experimental results showing their effectiveness for moderate size mechanisms. For example, we can verify coalition Nash equilibria for mechanisms which corresponding normal form games would have more than $5 \times 10^21$ entries. Moreover, we compare the two approaches, and the explicit algorithm turns out to outperform the symbolic one. To the best of our knowledge, no model checking algorithm for verification of Nash equilibria of mechanisms with coalitions has been previously published. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer |
Place of Publication |
|
Editor |
Guerraoui, R.; Petit, F. |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
5873 |
Series Issue |
|
Edition |
|
| ISSN |
|
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ sss09 |
Serial |
19 |
| Permanent link to this record |
| |
|
| |
| Author |
Alimguzhin, V.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E. |
| Title |
Linearising Discrete Time Hybrid Systems |
Type |
Journal Article |
| Year |
2017 |
Publication |
IEEE Transactions on Automatic Control |
Abbreviated Journal |
|
| Volume |
62 |
Issue |
10 |
Pages |
5357-5364 |
| Keywords |
|
| Abstract |
Model Based Design approaches for embedded systems aim at generating correct-by-construction control software, guaranteeing that the closed loop system (controller and plant) meets given system level formal specifications. This technical note addresses control synthesis for safety and reachability properties of possibly non-linear discrete time hybrid systems. By means of syntactical transformations that require non-linear terms to be Lipschitz continuous functions, we over-approximate non-linear dynamics with a linear system whose controllers are guaranteed to be controllers of the original system. We evaluate performance of our approach on meaningful control synthesis benchmarks, also comparing it to a state-of-the-art tool. |
| 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 |
0018-9286 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
no |
| Call Number |
Sapienza @ mari @ ref7902199 |
Serial |
164 |
| Permanent link to this record |
| |
|
| |
| Author |
Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E. |
| Title |
An Efficient Algorithm for Network Vulnerability Analysis Under Malicious Attacks |
Type |
Conference Article |
| Year |
2018 |
Publication |
Foundations of Intelligent Systems – 24th International Symposium, ISMIS 2018, Limassol, Cyprus, October 29-31, 2018, Proceedings |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
302-312 |
| 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 |
Best Paper |
Approved |
no |
| Call Number |
MCLab @ davi @ DBLP:conf/ismis/ManciniMMST18 |
Serial |
176 |
| Permanent link to this record |
| |
|
| |
| Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
| Title |
From Boolean Relations to Control Software |
Type |
Conference Article |
| Year |
2011 |
Publication |
Proceedings of ICSEA 2011, The Sixth International Conference on Software Engineering Advances |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
528-533 |
| Keywords |
|
| Abstract |
Many software as well digital hardware automatic synthesis methods define the set of implementations meeting the given system specifications with a boolean relation K. In such a context a fundamental step in the software (hardware) synthesis process is finding effective solutions to the functional equation defined by K. This entails finding a (set of) boolean function(s) F (typically represented using OBDDs, Ordered Binary Decision Diagrams) such that: 1) for all x for which K is satisfiable, K(x, F(x)) = 1 holds; 2) the implementation of F is efficient with respect to given implementation parameters such as code size or execution time. While this problem has been widely studied in digital hardware synthesis, little has been done in a software synthesis context. Unfortunately the approaches developed for hardware synthesis cannot be directly used in a software context. This motivates investigation of effective methods to solve the above problem when F has to be implemented with software. In this paper we present an algorithm that, from an OBDD representation for K, generates a C code implementation for F that has the same size as the OBDD for F and a WCET (Worst Case Execution Time) linear in nr, being n = |x| the number of input arguments for functions in F and r the number of functions in F. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
ThinkMind |
Place of Publication |
|
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
978-1-61208-165-6 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
Best Paper Award |
Approved |
yes |
| Call Number |
Sapienza @ mari @ icsea11 |
Serial |
14 |
| Permanent link to this record |
| |
|
| |
| Author |
Bono, V.; Salvo, I. |
| Title |
A CuCh Interpretation of an Object-Oriented Language |
Type |
Journal Article |
| Year |
2001 |
Publication |
Electronic Notes in Theoretical Computer Science |
Abbreviated Journal |
|
| Volume |
50 |
Issue |
2 |
Pages |
159-177 |
| Keywords |
|
| Abstract |
CuCh machine extends pure lambda–calculus with algebraic data types and provides a the possibility of defining functions over the disjoint sum of algebras. We exploit such natural form of overloading to define a functional interpretation of a simple, but significant fragment of a typical object-oriented language. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Elsevier |
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 |
BOTH 2001, Bohm’s theorem: applications to Computer Science Theory (Satellite Workshop of ICALP 2001) |
Approved |
yes |
| Call Number |
Sapienza @ mari @ Bono-Salvo:BOTH01 |
Serial |
72 |
| Permanent link to this record |
| |
|
| |
| Author |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
| Title |
On Model Based Synthesis of Embedded Control Software |
Type |
Conference Article |
| Year |
2012 |
Publication |
Proceedings of the 12th International Conference on Embedded Software, EMSOFT 2012, part of the Eighth Embedded Systems Week, ESWeek 2012, Tampere, Finland, October 7-12, 2012 |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
227-236 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
ACM |
Place of Publication |
|
Editor |
Ahmed Jerraya and Luca P. Carloni and Florence Maraninchi and John Regehr |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
|
ISBN |
978-1-4503-1425-1 |
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
Techreport version can be found at arxiv.org |
Approved |
yes |
| Call Number |
Sapienza @ mari @ emsoft12 |
Serial |
97 |
| Permanent link to this record |
| |
|
| |
| Author |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
| Title |
Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems |
Type |
Conference Article |
| Year |
2012 |
Publication |
Proceedings of the 51th IEEE Conference on Decision and Control, CDC 2012, December 10-13, 2012, Maui, HI, USA |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
6120-6125 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
IEEE |
Place of Publication |
|
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
|
ISBN |
978-1-4673-2065-8 |
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
Techreport version can be found at http://arxiv.org/abs/1207.4098 |
Approved |
yes |
| Call Number |
Sapienza @ mari @ cdc12 |
Serial |
96 |
| Permanent link to this record |
| |
|
| |
| Author |
Barbanera, Franco; Dezani-Ciancaglini, Mariangiola; Salvo, Ivano; Sassone, Vladimiro |
| Title |
A Type Inference Algorithm for Secure Ambients |
Type |
Journal Article |
| Year |
2002 |
Publication |
Electronic Notes in Theoretical Computer Science |
Abbreviated Journal |
|
| Volume |
62 |
Issue |
|
Pages |
83-101 |
| Keywords |
|
| Abstract |
We consider a type discipline for the Ambient Calculus that associates ambients with security levels and constrains them to be traversed by or opened in ambients of higher security clearance only. We present a bottom-up algorithm that, given an untyped process P, computes a minimal set of constraints on security levels such that all actions during runs of P are performed without violating the security level priorities. Such an algorithm appears to be a prerequisite to use type systems to ensure security properties in the web scenario. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Elsevier |
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 |
TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types |
Approved |
yes |
| Call Number |
Sapienza @ mari @ Barbanera-Dezani-Salvo-Sassone:01 |
Serial |
73 |
| Permanent link to this record |
