Symbolic Model Checking for Simply-Timed Systems

Abstract. We describe OBDD-based symbolic model checking algorithms for simply-timed systems, i.e. finite state graphs where transitions carry a duration. These durations can be arbitrary natural numbers. A simple and natural semantics for these systems opens the way for improved efficiency. Our algorithms have been implemented in NuSMV and perform well in practice (on standard case studies).

• Type: Conference
• Year: 2004
• Where: FORMATS
• Authors: Nicolas Markey, Ph. Schnoebelen
• Keywords: Arbitrary Natural Numbers, FORMATS 2004, Model Checking Algorithms, finite State Graphs