You are here

2002

  1. 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)
  2. 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)
  3. 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,
  4. 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

Pages