toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Records Links
Author Della Penna, Giuseppe; Magazzeni, Daniele; Tofani, Alberto; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico pdf  url
doi  openurl
  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 doi  openurl
  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. pdf  doi
openurl 
  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. pdf  doi
openurl 
  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. pdf  url
doi  openurl
  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. pdf  doi
openurl 
  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 pdf  openurl
  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 pdf  openurl
  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 pdf  doi
openurl 
  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. pdf  url
openurl 
  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
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: