Heuristics to Verify LTL Properties of Hierarchical Systems

Abstract

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.

Contributors

Ahmed Hammad

Hassan Mountassir

Conference

Publication date: July 2008

Publication date (Print): July 2008

Pages: 1-10

Affiliations

LIFC-Laboratoire d’Informatique de

l’Université de Franche-Comté 16, route de Gray F-25030 Besançon Cedex

Article

DOI: 10.14236/ewic/VECOS2008.14

Copyright statement: © Ahmed Hammad et al. Published by BCS Learning and Development Ltd. Second International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2008)

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

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

Conference acronym: VECoS

Conference number:

Conference location: Leeds, UK

Conference date: 2 - 3 July 2008

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Verification and Evaluation of Computer and Communication Systems

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/VECOS2008.14

Self URI (journal page): https://ewic.bcs.org/

Categories

Series title: Electronic Workshops in Computing