Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems." In Computer Aided Verification, edited by T. Touili, B. Cook and P. Jackson, 180–195. Lecture Notes in Computer Science 6174. Springer Berlin / Heidelberg, 2010. DOI: 10.1007/978-3-642-14295-6_20.
Abstract: We present an algorithm that given a Discrete Time Linear Hybrid System returns a correct-by-construction software implementation K for a (near time optimal) robust quantized feedback controller for along with the set of states on which K is guaranteed to work correctly (controllable region). Furthermore, K has a Worst Case Execution Time linear in the number of bits of the quantization schema.
|
Alessandro Fantechi, Stefania Gnesi, Franco Mazzanti, Rosario Pugliese, and Enrico Tronci. "A Symbolic Model Checker for ACTL." In International Workshop on Current Trends in Applied Formal Method (FM-Trends), edited by D. Hutter, W. Stephan, P. Traverso and M. Ullmann, 228–242. Lecture Notes in Computer Science 1641. Boppard, Germany: Springer, 1998. ISSN: 3-540-66462-9. DOI: 10.1007/3-540-48257-1_14.
Abstract: We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL formulae, and uses symbolic manipulation algorithms. SAM has been realized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on boolean functions, and by using the BSP interpreter to carry out computations (i.e. verifications).
|
Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement, and Harry Li. "Model Checking Coalition Nash Equilibria in MAD Distributed Systems." In Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, SSS 2009, Lyon, France, November 3-6, 2009. Proceedings, edited by R. Guerraoui and F. Petit, 531–546. Lecture Notes in Computer Science 5873. Springer, 2009. DOI: 10.1007/978-3-642-05118-0_37.
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.
|
Edoardo Campagnano, Ester Ciancamerla, Michele Minichino, and Enrico Tronci. "Automatic Analysis of a Safety Critical Tele Control System." In 24th International Conference on: Computer Safety, Reliability, and Security (SAFECOMP), edited by R. Winther, B. A. Gran and G. Dahll, 94–107. Lecture Notes in Computer Science 3688. Fredrikstad, Norway: Springer, 2005. ISSN: 3-540-29200-4. DOI: 10.1007/11563228_8.
Abstract: We show how the Mur$\varphi$ model checker can be used to automatically carry out safety analysis of a quite complex hybrid system tele-controlling vehicles traffic inside a safety critical transport infrastructure such as a long bridge or a tunnel. We present the Mur$\varphi$ model we developed towards this end as well as the experimental results we obtained by running the Mur$\varphi$ verifier on our model. Our experimental results show that the approach presented here can be used to verify safety of critical dimensioning parameters (e.g. bandwidth) of the telecommunication network embedded in a safety critical system.
|
Enrico Tronci. "Defining Data Structures via Böhm-Out." J. Funct. Program. 5, no. 1 (1995): 51–64. DOI: 10.1017/S0956796800001234.
Abstract: We show that any recursively enumerable subset of a data structure can be regarded as the solution set to a B??hm-out problem.
|
I. Melatti, F. Mari, T. Mancini, M. Prodanovic, and E. Tronci. "A Two-Layer Near-Optimal Strategy for Substation Constraint Management via Home Batteries." IEEE Transactions on Industrial Electronics (2021): 1. Notes: To appear. DOI: 10.1109/TIE.2021.3102431.
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.
|
