| Records |
| Author |
Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico |
| Title |
Flexible Timeline-Based Plan Verification |
Type |
Conference Article |
Year  |
2009 |
Publication |
KI 2009: Advances in Artificial Intelligence, 32nd Annual German Conference on AI, Paderborn, Germany, September 15-18, 2009. Proceedings |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
49-56 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer |
Place of Publication |
|
Editor |
Mertsching, Bärbel; Hund, M.; Aziz, M.Z. |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
5803 |
Series Issue |
|
Edition |
|
| ISSN |
978-3-642-04616-2 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ Cffot09 |
Serial |
21 |
| Permanent link to this record |
| |
|
| |
| 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 |
Melatti, Igor; Palmer, Robert; Sawaya, Geoffrey; Yang, Yu; Kirby, Robert Mike; Gopalakrishnan, Ganesh |
| Title |
Parallel and distributed model checking in Eddy |
Type |
Journal Article |
| Year |
2009 |
Publication |
Int. J. Softw. Tools Technol. Transf. |
Abbreviated Journal |
|
| Volume |
11 |
Issue |
1 |
Pages |
13-25 |
| 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 (1) performing overlapped asynchronous message passing, and (2) 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 |
Berlin, Heidelberg |
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
1433-2779 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ Mpsykg09 |
Serial |
80 |
| 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 |
Book Chapter |
| Year |
2008 |
Publication |
Informatics in Control Automation and Robotics. Selected Papers from ICINCO 2006 |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
107-119 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer |
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 @ Dmtmt08 |
Serial |
26 |
| 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 |
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 |
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 |
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 |
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 |
| |
|
| |
| Author |
Chierichetti, Flavio; Lattanzi, Silvio; Mari, Federico; Panconesi, Alessandro |
| Title |
On Placing Skips Optimally in Expectation |
Type |
Conference Article |
| Year |
2008 |
Publication |
Web Search and Web Data Mining (WSDM 2008) |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
15-24 |
| Keywords |
Information Retrieval |
| Abstract |
We study the problem of optimal skip placement in an inverted list. Assuming the query distribution to be known in advance, we formally prove that an optimal skip placement can be computed quite efficiently. Our best algorithm runs in time O(n log n), n being the length of the list. The placement is optimal in the sense that it minimizes the expected time to process a query. Our theoretical results are matched by experiments with a real corpus, showing that substantial savings can be obtained with respect to the tra- ditional skip placement strategy, that of placing consecutive skips, each spanning sqrt(n) many locations. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Acm |
Place of Publication |
|
Editor |
Najork, M.; Broder, A.Z.; Chakrabarti, S. |
| 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 @ ChiLatMar08 |
Serial |
94 |
| 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 |
