|   | 
Details
   web
Records
Author Della Penna, Giuseppe; Magazzeni, Daniele; Tofani, Alberto; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico
Title Automated Generation of Optimal Controllers through Model Checking Techniques Type Conference Article
Year 2006 Publication (up) Icinco-Icso Abbreviated Journal
Volume Issue Pages 26-33
Keywords
Abstract We present a methodology for the synthesis of controllers, which exploits (explicit) model checking techniques. That is, we can cope with the systematic exploration of a very large state space. This methodology can be applied to systems where other approaches fail. In particular, we can consider systems with an highly non-linear dynamics and lacking a uniform mathematical description (model). We can also consider situations where the required control action cannot be specified as a local action, and rather a kind of planning is required. Our methodology individuates first a raw optimal controller, then extends it to obtain a more robust one. A case study is presented which considers the well known truck-trailer obstacle avoidance parking problem, in a parking lot with obstacles on it. The complex non-linear dynamics of the truck-trailer system, within the presence of obstacles, makes the parking problem extremely hard. We show how, by our methodology, we can obtain optimal controllers with different degrees of robustness.
Address
Corporate Author Thesis
Publisher INSTICC Press Place of Publication Editor Andrade-Cetto, J.; Ferrier, J.-L.; Pereira, J. M. C. D.; Filipe, J.
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 972-8865-59-7 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dimmtt06 Serial 79
Permanent link to this record
 

 
Author Piperno, Adolfo; Tronci, Enrico
Title Regular Systems of Equations in λ-calculus Type Conference Article
Year 1989 Publication (up) Ictcs Abbreviated Journal
Volume Issue Pages
Keywords
Abstract Many problems arising in equational theories like Lambda-calculus and Combinatory Logic can be expressed by combinatory equations or systems of equations. However, the solvability problem for an arbitrarily given class of systems is in general undecidable. In this paper we shall focus our attention on a decidable class of systems, which will be called regular systems, and we shall analyse some classical problems and well-known properties of Lambda-calculus that can be described and solved by means of regular systems. The significance of such class will be emphasized showing that for slight extensions of it the solvability problem turns out to be undecidable.
Address
Corporate Author Thesis
Publisher Place of Publication Mantova - Italy 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 @ ictcs89 Serial 61
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 (up) 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 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 (up) 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 Hayes, B. P. ; Melatti, I.; Mancini, T.; Prodanovic, M.; Tronci, E.
Title Residential Demand Management using Individualised Demand Aware Price Policies Type Journal Article
Year 2017 Publication (up) IEEE Transactions On Smart Grid Abbreviated Journal
Volume 8 Issue 3 Pages 1284-1294
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 157
Permanent link to this record
 

 
Author Mancini, T.; Melatti, I.; Tronci, E.
Title Any-horizon uniform random sampling and enumeration of constrained scenarios for simulation-based formal verification Type Journal Article
Year 2021 Publication (up) IEEE Transactions on Software Engineering Abbreviated Journal
Volume Issue Pages 1-1
Keywords
Abstract Model-based approaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely on numerical simulation of the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying given constraints. Such constraints typically stem from requirements (or assumptions) on the SUV inputs and its operational environment as well as from the enforcement of additional conditions aiming at, e.g., prioritising the (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercising selected requirements, or avoiding </i>vacuity</i> in their satisfaction. In this setting, the possibility to efficiently sample at random (with a known distribution, e.g., uniformly) within, or to efficiently enumerate (possibly in a uniformly random order) scenarios among those satisfying all the given constraints is a key enabler for the practical viability of the verification process, e.g., via simulation-based statistical model checking. Unfortunately, in case of non-trivial combinations of constraints, iterative approaches like Markovian random walks in the space of sequences of inputs in general fail in extracting scenarios according to a given distribution (e.g., uniformly), and can be very inefficient to produce at all scenarios that are both legal (with respect to SUV assumptions) and of interest (with respect to the additional constraints). For example, in our case studies, up to 91% of the scenarios generated using such iterative approaches would need to be neglected. In this article, we show how, given a set of constraints on the input scenarios succinctly defined by multiple finite memory monitors, a data structure (scenario generator) can be synthesised, from which any-horizon scenarios satisfying the input constraints can be efficiently extracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enables seamless support to virtually all simulation-based approaches to CPS verification, ranging from simple random testing to statistical model checking and formal (i.e., exhaustive) verification, when a suitable bound on the horizon or an iterative horizon enlargement strategy is defined, as in the spirit of bounded model checking.
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 1939-3520 ISBN Medium
Area Expedition Conference
Notes To appear Approved no
Call Number MCLab @ davi @ ref9527998 Serial 191
Permanent link to this record
 

 
Author Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico
Title Validation and Verification Issues in a Timeline-based Planning System Type Conference Article
Year 2008 Publication (up) In E-Proc. of ICAPS Workshop on Knowledge Engineering for Planning and Scheduling Abbreviated Journal
Volume Issue Pages
Keywords
Abstract One of the key points to take into account to foster effective introduction of AI planning and scheduling systems in real world is to develop end user trust in the related technologies. Automated planning and scheduling systems often brings solutions to the users which are neither “obviousÃ¢â‚¬Âť nor immediately acceptable for them. This is due to the ability of these tools to take into account quite an amount of temporal and causal constraints and to employ resolution processes often designed to optimize the solution with respect to non trivial evaluation functions. To increase technology trust, the study of tools for verifying and validating plans and schedules produced by AI systems might be instrumental. In general, validation and verification techniques represent a needed complementary technology in developing domain independent architectures for automated problem solving. This paper presents a preliminary report of the issues concerned with the use of two software tools for formal verification of finite state systems to the validation of the solutions produced by MrSPOCK, a recent effort for building a timeline based planning tool in an ESA project.
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 @ Keps08 Serial 25
Permanent link to this record
 

 
Author Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico
Title Merging Planning, Scheduling & Verification – A Preliminary Analysis Type Conference Article
Year 2008 Publication (up) In Proc. of 10th ESA Workshop on Advanced Space Technologies for Robotics and Automation (ASTRA) 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 yes
Call Number Sapienza @ mari @ Astra08 Serial 24
Permanent link to this record
 

 
Author Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico
Title Anytime System Level Verification via Random Exhaustive Hardware In The Loop Simulation Type Conference Article
Year 2014 Publication (up) In Proceedings of 17th EuroMicro Conference on Digital System Design (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 Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Serial 122
Permanent link to this record
 

 
Author Mancini, T.
Title Now or Never: negotiating efficiently with unknown counterparts Type Journal Article
Year 2015 Publication (up) In proceedings of the 22nd RCRA International Workshop. Ferrara, Italy. CEUR, 2015 (Co-located with the 14th Conference of the Italian Association for Artificial Intelligence (AI*IA 2015)). 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 @ preissler @ Mancini2015 Serial 131
Permanent link to this record