Intensional Approaches for Symbolic Methods
Résumé
We present a behavioral model for discrete event systems based on an intentional formalism, as a possible approach within the broader trend towards rich symbolic representations in verification. We define Intensional Labeled Transition Systems with associated combinators of parallel composition and event hiding, and we propose symbolic bisimulation to handle strong bisimulation intentionally. Further on, we explain how the methodology has been developed for the synchronous language Signal, via the verification tool Sigali.