Records |
Author |
Böhm, Corrado; Piperno, Adolfo; Tronci, Enrico |
Title |
Solving Equations in λ-calculus |
Type |
Conference Article |
Year |
1989 |
Publication |
Proc. of: Logic Colloquium 88 |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
|
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
|
Place of Publication |
Padova - 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 @ logic-colloquium-88 |
Serial |
62 |
Permanent link to this record |
|
|
|
Author |
Böhm, Corrado; Tronci, Enrico |
Title |
X-Separability and Left-Invertibility in lambda-calculus |
Type |
Conference Article |
Year |
1987 |
Publication |
Symposium on Logic in Computer Science (LICS) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
320-328 |
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
IEEE Computer Society |
Place of Publication |
Ithaca, New York, USA |
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 @ lics87 |
Serial |
63 |
Permanent link to this record |
|
|
|
Author |
Böhm, Corrado; Tronci, Enrico |
Title |
X-separability and left-invertibility in the λ-calculus (extended abstract, invited paper) |
Type |
Conference Article |
Year |
1987 |
Publication |
Proceedings of: Temi e prospettive della Logica e della Filosofia della Scienza contemporanea |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
|
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
|
Place of Publication |
Cesena - 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 @ cesena87 |
Serial |
64 |
Permanent link to this record |
|
|
|
Author |
Tronci, Enrico |
Title |
On Computing Optimal Controllers for Finite State Systems |
Type |
Conference Article |
Year |
1997 |
Publication |
CDC '97: Proceedings of the 36th IEEE International Conference on Decision and Control |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
|
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
IEEE Computer Society |
Place of Publication |
Washington, DC, USA |
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 @ cdc97 |
Serial |
66 |
Permanent link to this record |
|
|
|
Author |
Tronci, Enrico |
Title |
Optimal Finite State Supervisory Control |
Type |
Conference Article |
Year |
1996 |
Publication |
CDC '96: Proceedings of the 35th IEEE International Conference on Decision and Control |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
|
Keywords |
|
Abstract |
Supervisory Controllers are Discrete Event Dynamic Systems (DEDSs) forming the discrete core of a Hybrid Control System. We address the problem of automatic synthesis of Optimal Finite State Supervisory Controllers (OSCs). We show that Boolean First Order Logic (BFOL) and Binary Decision Diagrams (BDDs) are an effective methodological and practical framework for Optimal Finite State Supervisory Control. Using BFOL programs (i.e. systems of boolean functional equations) and BDDs we give a symbolic (i.e. BDD based) algorithm for automatic synthesis of OSCs. Our OSC synthesis algorithm can handle arbitrary sets of final states as well as plant transition relations containing loops and uncontrollable events (e.g. failures). We report on experimental results on the use of our OSC synthesis algorithm to synthesize a C program implementing a minimum fuel OSC for two autonomous vehicles moving on a 4 x 4 grid. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
IEEE Computer Society |
Place of Publication |
Washington, DC, USA |
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 @ cdc96 |
Serial |
67 |
Permanent link to this record |
|
|
|
Author |
Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico |
Title |
A Model Checking Technique for the Verification of Fuzzy Control Systems |
Type |
Conference Article |
Year |
2005 |
Publication |
CIMCA '05: Proceedings of the International Conference on Computational Intelligence for Modelling, Control and Automation and International Conference on Intelligent Agents, Web Technologies and Internet Commerce Vol-1 (CIMCA-IAWTIC'06) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
536-542 |
Keywords |
|
Abstract |
Fuzzy control is well known as a powerful technique for designing and realizing control systems. However, statistical evidence for their correct behavior may be not enough, even when it is based on a large number of samplings. In order to provide a more systematic verification process, the cell-to-cell mapping technology has been used in a number of cases as a verification tool for fuzzy control systems and, more recently, to assess their optimality and robustness. However, cell-to-cell mapping is typically limited in the number of cells it can explore. To overcome this limitation, in this paper we show how model checking techniques may be instead used to verify the correct behavior of a fuzzy control system. To this end, we use a modified version of theMurphi verifier, which ease the modeling phase by allowing to use finite precision real numbers and external C functions. In this way, also already designed simulators may be used for the verification phase. With respect to the cell mapping technique, our approach appears to be complementary; indeed, it explores a much larger number of states, at the cost of being less informative on the global dynamic of the system. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
IEEE Computer Society |
Place of Publication |
Washington, DC, USA |
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
0-7695-2504-0-01 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
yes |
Call Number |
Sapienza @ mari @ Immt05 |
Serial |
75 |
Permanent link to this record |
|
|
|
Author |
Brizzolari, Francesco; Melatti, Igor; Tronci, Enrico; Della Penna, Giuseppe |
Title |
Disk Based Software Verification via Bounded Model Checking |
Type |
Conference Article |
Year |
2007 |
Publication |
APSEC '07: Proceedings of the 14th Asia-Pacific Software Engineering Conference |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
358-365 |
Keywords |
|
Abstract |
One of the most successful approach to automatic software verification is SAT based bounded model checking (BMC). One of the main factors limiting the size of programs that can be automatically verified via BMC is the huge number of clauses that the backend SAT solver has to process. In fact, because of this, the SAT solver may easily run out of RAM. We present two disk based algorithms that can considerably decrease the number of clauses that a BMC backend SAT solver has to process in RAM. Our experimental results show that using our disk based algorithms we can automatically verify programs that are out of reach for RAM based BMC. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
IEEE Computer Society |
Place of Publication |
Washington, DC, USA |
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
0-7695-3057-5 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
yes |
Call Number |
Sapienza @ mari @ Bmtd07 |
Serial |
76 |
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 |
|
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 |
Della Penna, Giuseppe; Magazzeni, Daniele; Tofani, Alberto; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico |
Title |
Automatic Synthesis of Robust Numerical Controllers |
Type |
Conference Article |
Year |
2007 |
Publication |
Icas '07 |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
4 |
Keywords |
|
Abstract |
A major problem of numerical controllers is their robustness, i.e. the state read from the plant may not be in the controller table, although it may be close to some states in the table. For continuous systems, this problem is typically handled by interpolation techniques. Unfortunately, when the plant contains both continuous and discrete variables, the interpolation approach does not work well. To cope with this kind of systems, we propose a general methodology that exploits explicit model checking in an innovative way to automatically synthesize a (time-) optimal numerical controller from a plant specification and apply an optimized strengthening algorithm only on the most significant states, in order to reach an acceptable robustness degree. We implemented all the algorithms within our CGMurphi tool, an extension of the well-known CMurphi verifier, and tested the effectiveness of our approach by applying it to the well-known truck and trailer obstacles avoidance problem. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
IEEE Computer Society |
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
0-7695-2859-5 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
yes |
Call Number |
Sapienza @ mari @ Dmtimt07 |
Serial |
89 |
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 |