Symbolic Temporal Constraint Analysis, An Approach for Verifying Hybrid Systems
| Authors: | Riviere Nicolas, LAAS-CNRS, France
Demmou Hamid, LAAS-CNRS, France
Valette Robert, LAAS-CNRS, France
Medjoudj Malika, LAAS-CNRS, France |
|---|
| Topic: | 1.3 Discrete Event and Hybrid Systems |
|---|
| Session: | Analysis and Design of Hybrid Systems I |
|---|
| Keywords: | Hybrid system, Verification, Constraint Satisfaction Problems, Petri nets |
|---|
Abstract
The purpose of the paper is to illustrate a method, based on theoremproving, allowing the determination of a set of constraintssuch that some property of an hybrid system is verified.The approach is based on the generation of scenarios byproving some linear logic sequents and on the analysisof symbolic temporal constraints in a Simple Temporal Network.In the presented example, the property is the reachability of agiven state within some temporal constraint.The paper focuses on the detailed presentation ofthe example.
