Implementing a Modal Logic over Data and Processes using XTL

The modal logic FULL is designed to capture strong bisimulation over early symbolic transition systems (STSs) for full LOTOS. It provides a compact way of expressing and verifying properties involving both data and transitions. In this paper we present a restricted prototype implementation of a model checker for LOTOS for queries written using the FULL logic. The model checker is developed within the CADP package using XTL.

• Type: Conference
• Year: 2001
• Where: FORTE
• Authors: Jeremy Bryans, Carron Shankland
• Keywords: Early Symbolic Transition, FORTE 2001, FORTE 2007, Model Checker, Restricted Prototype Implementation