You are here

2001

  1. 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)
  2. 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)
  3. 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)
  4. Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri,
    Conditional Planning under Partial Obserbability as Heuristic-Symbolic Search in Belief Space,
    Sixth European Conference on Planning [ECP-01],
    Springer,
    2001
    , pp. 379-
    384
    , (Sixth European Conference on Planning [ECP-01],
    2001)
  5. Massimo Benerecetti; Alessandro Cimatti,
    Symbolic model checking for multi-agent systems,
    Second Workshop on Computational Logic in Multi-Agent Systems (CLIMA`01),
    2001
    , (Second Workshop on Computational Logic in Multi-Agent Systems (CLIMA`01),
    Paphos, Cyprus,
    2001)
  6. Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore; Marco Roveri; Paolo Traverso,
    IJCAI-2001 Workshop on Planning under Uncertainty and Incomplete Information (PRO-2),
    2001
    , (IJCAI-2001 Workshop on Planning under Uncertainty and Incomplete Information (PRO-2),
    Seattle, Washington, USA,
    2001)
  7. Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri; Paolo Traverso,
    Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), Proceedings,
    Morgan Kaufmann,
    2001
    , pp. 473-
    478
    , (Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), Proceedings,
    Seattle, Washington, USA,
    2001)
  8. Alessandro Cimatti,
    Industrial Applications of Model Checking,
    Formal methods have a great potential of application in the development of industrial critical systems. in certain application fields, formal methods are even becoming part of standards. Among formal methods, Model Checking is proving particularly effective, especially thanks to its ability to automatically analyze complex designs and to produce counterexamples. However, the application of formal methods in the industrial development practice is by no means trivial. Formal methods can be costly, slow down the development, and require training and changes to the development cycle. In this paper, the application of Model Checking techniques in the development of the application of Model Checking techniques in the development of industrial critical systems is discussed, by focusing on two projects where Model Checking has been successfully applied under different conditions.,
    2001
  9. Piergiorgio Bertoli; Alessandro Cimatti,
    Improving Heuristics for Planning and Search in Belief Space,
    Search in the space of beliefs has been proposed as a convenient framework for tackling planning under uncertainty. Significant improvements have been recently achieved, especially thanks to the use of symbolic model checking techniques such as Binary Decision Diagrams. However, the problem is extremely complex, and the heuristics available so far are unable to provide enough guidance for an informed search. In this paper we tackle the problem of defining effective heuristics for driving the search in belief space. The basic intuition is that the "degree of knowledge" associated with the belief states reached by partial plans must be explicitly taken into account when deciding the search direction. We propose a way of ranking belief states depending on their degree of knowledge with respect to a given set of boolean functions. This allows us to define a planning algorithm based on the identification and solution of suitable "knowledge subgoals", that are used as intermediate steps during the search. The solution of knowledge subgoals is based on the identification of "knowledge acquisition conditions", i.e. subsets of the state space from where it is possible to perform knowledge acquisition actions. We show the effectiveness of the proposed ideas by observing substantial improvements in the conformant planning algorithms of MBP,
    2001