You are here

Publications

  1. Marco Bozzano; G. Delzanno,
    Automated Protocol Verification in Linear Logic,
    Proceedings of the Fourth International Conference on Principles and Practice of Declarative Programming [PPDP 2002],
    2002
  2. Alessandro Cimatti; E.M. Clarke; Enrico Giunchiglia; Fausto Giunchiglia; Marco Pistore; Marco Roveri; Roberto Sebastiani; A. Tacchella,
    NuSMV 2: An OpenSource Tool for Symbolic model Checking,
    CAV 2002, Conference on Computer-Aided Verification,
    Springer,
    vol.2404,
    2002
    , pp. 359-
    364
    , (CAV 2002, Conference on Computer-Aided Verification,
    Copenhagen, Denmark,
    2002)
  3. Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore; Paolo Traverso,
    Electronic Proceedings of AIPS`02 Workshop on Planning via Model Checking,
    2002
    , (Electronic Proceedings of AIPS`02 Workshop on Planning via Model Checking,
    2002)
  4. Bozzano, Marco; Delzanno, Giorgio,
    Beyond parameterized verification,
    International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2002: Tools and Algorithms for the Construction and Analysis of Systems,
    Heidelberg,
    Springer,
    vol.2280,
    2002
    , pp. 221-
    235
    , (International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2002: Tools and Algorithms for the Construction and Analysis of Systems,
    Grenoble, France,
    April 8–12, 2002)
  5. Bozzano, Marco; Delzanno, Giorgio,
    Algorithmic Verification of Invalidation-Based Protocols,
    Computer Aided Verification,
    Heidelberg,
    Spinger,
    vol.2404,
    2002
    , pp. 295-
    308
    , (14th International Conference, CAV 2002,
    Copenhagen, Denmark,
    July 27–31, 2002)
  6. Marco Roveri; Alessandro Cimatti; Roberto Cavada; Andrei Tchaltsev; Andrea Micheli; Alessandro Mariotti; Sergio Mover; Marco Pensallorto; Armando Tacchella; Daniel Sheridan; Gavin Keighren; Tommi Junttila; Timo Latvala,
    2002,
  7. Marco Roveri,
    Planning in Non-Deterministic Domains via Symbolic Model Checking,
    In the thesis is tackled the Artificial Intelligence (AI) problem of Automatic Planning using Symbolic Model Checking (SMC) techniques developed within the Formal Verification community for the verification of designs. The use of SMC techniques allowed for a formal definition and for an efficient handling of a large class of planning problems that classical planning systems developed within AI Planning are not able to deal with. In the thesis two restricting hypothesis of classical planning have been discarded. Planning domains are assumed to be non-deterministic and are modeled as non-deterministic finite state automata. Moreover, a planning domain can be partially observable at execution time. A formal characterization of solutions to different planning problem is provided, distinguishing among weak solutions (that may achieve the goal), strong solution (that guarantee goal achievement) and strong cyclic solutions (that capture a trial and error behavior guaranteeing goal achievement under `fair` executions); under different hypothesis of domain run-time observability (i.e., full, null and partial observability). A family of algorithms to synthesize solutions to the different planning problems characterized are provided and proved to be correct. The algorithms have been implemented in the Model Based Planner (MBP) using SMC techniques. An extensive experimental analysis is carried out to show the effectiveness of the proposed approach w.r.t. the other state of the art planners,
    2002
  8. Alessandro Cimatti; Marco Roveri; Piergiorgio Bertoli,
    Searching Porwerset Automata by Combining Explicit-State and Symbolic Model Checking,
    Tools and Algorithms for the Construction and Analysis of Systems [TACAS 2001], Conference Proceedings,
    Springer,
    vol.2031,
    2001
    , pp. 313-
    327
    , (Tools and Algorithms for the Construction and Analysis of Systems [TACAS 2001], Conference Proceedings,
    2001)
  9. Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri,
    Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning,
    17th International Joint Conference on Artificial Intelligence, IJCAI 2001,
    Morgan Kaufmann,
    2001
    , pp. 467-
    472
    , (17th International Joint Conference on Artificial Intelligence, IJCAI 2001,
    Seattle, USA,
    04/08/2001 - 10/08/2001)
  10. Alessandro Cimatti; E. Giunchiglia; Marco Pistore; Marco Roveri; Roberto Sebastiani; A. Tacchella,
    NuSMV Version 2: BDD-based + SAT-based Symbolic Model Checking,
    Proceedings of the IJCAR Workshop `Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics`,
    no publisher,
    2001
    , (Proceedings of the IJCAR Workshop `Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics`,
    Siena, Italy,
    19/06/2001)

Pages