Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Heuristics to Verify LTL Properties of Hierarchical Systems

    Second International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2008)

    Leeds, UK, 2 - 3 July 2008


    Ahmed Hammad and Hassan Mountassir


    Hierarchical automata are used to model hierarchical systems. The semantics used is the Kripke structure where states are valued by atomic propositions. This structure can be large in number of states. This paper presents some heuristics to check properties expressed in LTL logic (Linear Temporal Logic). Hierarchical systems are defined in an hierarchical way by a set of subsystems by decomposing every time one or more states in a set of automata. To cope with the combinatorial explosion problem and the check of properties, we consider only the sub-systems concerned by the property to verify and we then deduct its check from it on the global system.


    PDF filePDF Version of this Paper (431kb)