|   | 
Details
   web
Records
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 (up) 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 Tronci, Enrico
Title Defining Data Structures via Böhm-Out Type Journal Article
Year 1995 Publication J. Funct. Program. Abbreviated Journal
Volume 5 Issue 1 Pages 51-64
Keywords
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.
Address
Corporate Author Thesis
Publisher Place of Publication (up) 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 @ jfp95 Serial 57
Permanent link to this record
 

 
Author Böhm, Corrado; Tronci, Enrico
Title About Systems of Equations, X-Separability, and Left-Invertibility in the lambda-Calculus Type Journal Article
Year 1991 Publication Inf. Comput. Abbreviated Journal
Volume 90 Issue 1 Pages 1-32
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication (up) 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 @ infcomp91 Serial 59
Permanent link to this record
 

 
Author Piperno, Adolfo; Tronci, Enrico
Title Regular Systems of Equations in λ-calculus Type Journal Article
Year 1990 Publication Int. J. Found. Comput. Sci. Abbreviated Journal
Volume 1 Issue 3 Pages 325-340
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 (up) 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 @ ijfcs90 Serial 60
Permanent link to this record
 

 
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 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 (up) 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 Melatti, Igor; Palmer, Robert; Sawaya, Geoffrey; Yang, Yu; Kirby, Robert Mike; Gopalakrishnan, Ganesh
Title Parallel and Distributed Model Checking in Eddy Type Conference Article
Year 2006 Publication Model Checking Software, 13th International SPIN Workshop, Vienna, Austria, March 30 – April 1, 2006, Proceedings Abbreviated Journal
Volume Issue Pages 108-125
Keywords
Abstract Model checking of safety properties can be scaled up by pooling the CPU and memory resources of multiple computers. As compute clusters containing 100s of nodes, with each node realized using multi-core (e.g., 2) CPUs will be widespread, a model checker based on the parallel (shared memory) and distributed (message passing) paradigms will more efficiently use the hardware resources. Such a model checker can be designed by having each node employ two shared memory threads that run on the (typically) two CPUs of a node, with one thread responsible for state generation, and the other for efficient communication, including (i) performing overlapped asynchronous message passing, and (ii) aggregating the states to be sent into larger chunks in order to improve communication network utilization. We present the design details of such a novel model checking architecture called Eddy. We describe the design rationale, details of how the threads interact and yield control, exchange messages, as well as detect termination. We have realized an instance of this architecture for the Murphi modeling language. Called Eddy_Murphi, we report its performance over the number of nodes as well as communication parameters such as those controlling state aggregation. Nearly linear reduction of compute time with increasing number of nodes is observed. Our thread task partition is done in such a way that it is modular, easy to port across different modeling languages, and easy to tune across a variety of platforms.
Address
Corporate Author Thesis
Publisher Springer - Verlag Place of Publication (up) Editor Valmari, A.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 3925 Series Issue Edition
ISSN 0302-9743 ISBN 978-3-540-33102-5 Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Mpsykg06 Serial 81
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico
Title Exploiting Hub States in Automatic Verification Type Conference Article
Year 2005 Publication Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings Abbreviated Journal
Volume Issue Pages 54-68
Keywords
Abstract In this paper we present a new algorithm to counteract state explosion when using Explicit State Space Exploration to verify protocol-like systems. We sketch the implementation of our algorithm within the Caching Mur$\varphi$ verifier and give experimental results showing its effectiveness. We show experimentally that, when memory is a scarce resource, our algorithm improves on the time performances of Caching Mur$\varphi$ verification algorithm, saving between 16% and 68% (45% on average) in computation time.
Address
Corporate Author Thesis
Publisher Springer Place of Publication (up) Editor D.A. Peled; Y.-K. Tsay
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 3707 Series Issue Edition
ISSN 3-540-29209-8 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dimt04 Serial 83
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
Title Finite Horizon Analysis of Markov Chains with the Mur$\varphi$ Verifier Type Conference Article
Year 2003 Publication Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings Abbreviated Journal
Volume Issue Pages 394-409
Keywords
Abstract In this paper we present an explicit disk based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
Address
Corporate Author Thesis
Publisher Springer Place of Publication (up) Editor Geist, D.; Tronci, E.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 2860 Series Issue Edition
ISSN 3-540-20363-X ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dimtz03 Serial 84
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
Title Integrating RAM and Disk Based Verification within the Mur$\varphi$ Verifier Type Conference Article
Year 2003 Publication Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings Abbreviated Journal
Volume Issue Pages 277-282
Keywords
Abstract We present a verification algorithm that can automatically switch from RAM based verification to disk based verification without discarding the work done during the RAM based verification phase. This avoids having to choose beforehand the proper verification algorithm. Our experimental results show that typically our integrated algorithm is as fast as (sometime faster than) the fastest of the two base (i.e. RAM based and disk based) verification algorithms.
Address
Corporate Author Thesis
Publisher Springer Place of Publication (up) Editor Geist, D.; Tronci, E.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 2860 Series Issue Edition
ISSN 3-540-20363-X ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ DIMTZ03a Serial 85
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Di Marco, Antinisca; Intrigila, Benedetto; Melatti, Igor; Pierantonio, Alfonso
Title Xere: Towards a Natural Interoperability between XML and ER Diagrams Type Conference Article
Year 2003 Publication Fundamental Approaches to Software Engineering, 6th International Conference, FASE 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings Abbreviated Journal
Volume Issue Pages 356-371
Keywords
Abstract XML (eXtensible Markup Language) is becoming the standard format for documents on Internet and is widely used to exchange data. Often, the relevant information contained in XML documents needs to be also stored in legacy databases (DB) in order to integrate the new data with the pre-existing ones. In this paper, we introduce a technique for the automatic XML-DB integration, which we call Xere. In particular we present, as the first step of Xere, the mapping algorithm which allows the translation of XML Schemas into Entity-Relationship diagrams.
Address
Corporate Author Thesis
Publisher Springer Place of Publication (up) Editor Pezzè, M.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 2621 Series Issue Edition
ISSN 3-540-00899-3 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Ddimp03 Serial 86
Permanent link to this record