Records |
Author |
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 |
Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.; Hayes, B.; Prodanovic, M.; Elmegaard, L. |
Title |
Parallel Statistical Model Checking for Safety Verification in Smart Grids |
Type |
Conference Article |
Year |
2018 |
Publication |
2018 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
1-6 |
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 @ mancini-etal:2018:smartgridcomm |
Serial |
170 |
Permanent link to this record |
|
|
|
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 |
Title |
Model Based Synthesis of Control Software from System Level Formal Specifications |
Type |
Journal Article |
Year |
2014 |
Publication |
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY |
Abbreviated Journal |
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY |
Volume |
23 |
Issue |
1 |
Pages |
Article 6 |
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
ACM |
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
1049-331X |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
Sapienza @ melatti @ |
Serial |
110 |
Permanent link to this record |
|
|
|
Author |
Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. |
Title |
Anytime system level verification via parallel random exhaustive hardware in the loop simulation |
Type |
Journal Article |
Year |
2016 |
Publication |
Microprocessors and Microsystems |
Abbreviated Journal |
|
Volume |
41 |
Issue |
|
Pages |
12-28 |
Keywords |
Model Checking of Hybrid Systems; Model checking driven simulation; Hardware in the loop simulation |
Abstract |
Abstract System level verification of cyber-physical systems has the goal of verifying that the whole (i.e., software + hardware) system meets the given specifications. Model checkers for hybrid systems cannot handle system level verification of actual systems. Thus, Hardware In the Loop Simulation (HILS) is currently the main workhorse for system level verification. By using model checking driven exhaustive HILS, System Level Formal Verification (SLFV) can be effectively carried out for actual systems. We present a parallel random exhaustive HILS based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on SLFV of the Inverted Pendulum on a Cart and the Fuel Control System examples in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability. |
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 |
0141-9331 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
MCLab @ davi @ Mancini201612 |
Serial |
155 |
Permanent link to this record |
|
|
|
Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
Title |
Control Software Visualization |
Type |
Conference Article |
Year |
2012 |
Publication |
Proceedings of INFOCOMP 2012, The Second International Conference on Advanced Communications and Computation |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
15-20 |
Keywords |
|
Abstract |
|
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-226-4 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
yes |
Call Number |
Sapienza @ mari @ infocomp2012 |
Serial |
100 |
Permanent link to this record |
|
|
|
Author |
Chierichetti, Flavio; Lattanzi, Silvio; Mari, Federico; Panconesi, Alessandro |
Title |
On Placing Skips Optimally in Expectation |
Type |
Conference Article |
Year |
2008 |
Publication |
Web Search and Web Data Mining (WSDM 2008) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
15-24 |
Keywords |
Information Retrieval |
Abstract |
We study the problem of optimal skip placement in an inverted list. Assuming the query distribution to be known in advance, we formally prove that an optimal skip placement can be computed quite efficiently. Our best algorithm runs in time O(n log n), n being the length of the list. The placement is optimal in the sense that it minimizes the expected time to process a query. Our theoretical results are matched by experiments with a real corpus, showing that substantial savings can be obtained with respect to the tra- ditional skip placement strategy, that of placing consecutive skips, each spanning sqrt(n) many locations. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
Acm |
Place of Publication |
|
Editor |
Najork, M.; Broder, A.Z.; Chakrabarti, S. |
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 @ ChiLatMar08 |
Serial |
94 |
Permanent link to this record |
|
|
|
Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Tronci, Enrico; Venturini Zilli, Marisa |
Title |
Synchronized regular expressions |
Type |
Journal Article |
Year |
2003 |
Publication |
Acta Inf. |
Abbreviated Journal |
|
Volume |
39 |
Issue |
1 |
Pages |
31-70 |
Keywords |
|
Abstract |
Text manipulation is one of the most common tasks for everyone using a computer. The increasing number of textual information in electronic format that every computer user collects everyday also increases the need of more powerful tools to interact with texts. Indeed, much work has been done to provide simple and versatile tools that can be useful for the most common text manipulation tasks. Regular Expressions (RE), introduced by Kleene, are well known in the formal language theory. RE have been extended in various ways, depending on the application of interest. In almost all the implementations of RE search algorithms (e.g. the egrep [15] UNIX command, or the Perl [20] language pattern matching constructs) we find backreferences, i.e. expressions that make reference to the string matched by a previous subexpression. Generally speaking, it seems that all kinds of synchronizations between subexpressions in a RE can be very useful when interacting with texts. In this paper we introduce the Synchronized Regular Expressions (SRE) as an extension of the Regular Expressions. We use SRE to present a formal study of the already known backreferences extension, and of a new extension proposed by us, which we call the synchronized exponents. Moreover, since we are dealing with formalisms that should have a practical utility and be used in real applications, we have the problem of how to present SRE to the final users. Therefore, in this paper we also propose a user-friendly syntax for SRE to be used in implementations of SRE-powered search algorithms. |
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 @ actainf03 |
Serial |
39 |
Permanent link to this record |
|
|
|
Author |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
Title |
A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software |
Type |
Conference Article |
Year |
2013 |
Publication |
Proc. of International SPIN Symposium on Model Checking of Software (SPIN 2013) |
Abbreviated Journal |
International SPIN Symposium on Model Checking of Software |
Volume |
|
Issue |
|
Pages |
43-60 |
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
Springer - Verlag |
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
Series Volume |
7976 |
Series Issue |
|
Edition |
|
ISSN |
0302-9743 |
ISBN |
978-3-642-39175-0 |
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
Sapienza @ melatti @ |
Serial |
112 |
Permanent link to this record |
|
|
|
Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa |
Title |
Finite Horizon Analysis of Stochastic Systems with the Mur$\varphi$ Verifier |
Type |
Conference Article |
Year |
2003 |
Publication |
Theoretical Computer Science, 8th Italian Conference, ICTCS 2003, Bertinoro, Italy, October 13-15, 2003, Proceedings |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
58-71 |
Keywords |
|
Abstract |
Many reactive systems are actually Stochastic Processes. Automatic analysis of such systems is usually very difficult thus typically one simplifies the analysis task by using simulation or by working on a simplified model (e.g. a Markov Chain). We present a Finite Horizon Probabilistic Model Checking approach which essentially can handle the same class of stochastic processes of a typical simulator. This yields easy modeling of the system to be analyzed together with formal verification capabilities. Our approach is based on a suitable disk based extension of the Mur$\varphi$ verifier. Moreover we present experimental results showing effectiveness of our approach. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
Springer |
Place of Publication |
|
Editor |
Blundo, C.; Laneve, C. |
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
Series Volume |
2841 |
Series Issue |
|
Edition |
|
ISSN |
3-540-20216-1 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
yes |
Call Number |
Sapienza @ mari @ DIMTZ03c |
Serial |
90 |
Permanent link to this record |