|
Records |
Links |
|
Author |
Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico |
|
|
Title |
Flexible Plan Verification: Feasibility Results |
Type |
Conference Article |
|
Year |
2009 |
Publication |
16th RCRA International Workshop on “Experimental evaluation of algorithms for solving problems with combinatorial explosion” (RCRA). Proceedings |
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 @ Rcra09 |
Serial |
22 |
|
Permanent link to this record |
|
|
|
|
Author |
Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico |
|
|
Title |
Verifying Flexible Timeline-based Plans |
Type |
Conference Article |
|
Year |
2009 |
Publication |
E-Proc. of ICAPS Workshop on Validation and Verification of Planning and Scheduling Systems |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
The synthesis of flexible temporal plans has demonstrated wide applications possibilities in heterogeneous domains. We are currently studying the connection between plan generation and execution from the particular perspective of verifying a flexible plan before actual execution. This paper explores how a model-checking verification tool, based on UPPAAL-TIGA, is suitable for verifying flexible temporal plans. We first describe the formal model, the formalism, and the verification method. Furthermore we discuss our own approach and some preliminary empirical results using a real-world case study. |
|
|
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 @ Vvps09 |
Serial |
23 |
|
Permanent link to this record |
|
|
|
|
Author |
Bobbio, Andrea; Ciancamerla, Ester; Minichino, Michele; Tronci, Enrico |
|
|
Title |
Functional analysis of a telecontrol system and stochastic measures of its GSM/GPRS connections |
Type |
Journal Article |
|
Year |
2005 |
Publication |
Archives of Transport – International Journal of Transport Problems |
Abbreviated Journal |
|
|
|
Volume |
17 |
Issue |
3-4 |
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 @ jtp05 |
Serial |
31 |
|
Permanent link to this record |
|
|
|
|
Author |
|
|
|
Title |
Charme |
Type |
Conference Article |
|
Year |
2003 |
Publication |
Lecture Notes in Computer Science |
Abbreviated Journal |
|
|
|
Volume |
2860 |
Issue |
|
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
Springer |
Place of Publication |
|
Editor |
Geist, D.; Tronci, E. |
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
3-540-20363-X |
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
yes |
|
|
Call Number |
Sapienza @ mari @ editor-charme03 |
Serial |
37 |
|
Permanent link to this record |
|
|
|
|
Author |
Piperno, Adolfo; Tronci, Enrico |
|
|
Title |
Regular Systems of Equations in λ-calculus |
Type |
Conference Article |
|
Year |
1989 |
Publication |
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 |
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 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 |
Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Giovannetti, Elio; Salvo, Ivano |
|
|
Title |
Mobility Types for Mobile Processes in Mobile Ambients |
Type |
Journal Article |
|
Year |
2003 |
Publication |
Electr. Notes Theor. Comput. Sci. |
Abbreviated Journal |
|
|
|
Volume |
78 |
Issue |
|
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
We present an ambient-like calculus in which the open capability is dropped, and a new form of “lightweight  process mobility is introduced. The calculus comes equipped with a type system that allows the kind of values exchanged in communications and the access and mobility properties of processes to be controlled. A type inference procedure determines the “minimal  requirements to accept a system or a component as well typed. This gives a kind of principal typing. As an expressiveness test, we show that some well known calculi of concurrency and mobility can be encoded in our calculus in a natural way. |
|
|
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 @ Coppo-Dezani-Giovannetti-Salvo:03 |
Serial |
74 |
|
Permanent link to this record |