Multi-valued model checking in dense-time

Abstract:

In this paper we introduce ΧTCTL, a dense-time extension of the multi-valued Computation Tree Logic (ΧCTL) in [1]. Alternatively, ΧTCTL is a multi-valued extension of TCTL [2] over quasi-boolean algebras. A multi-valued quotient is defined which enables to reduce dense-time ΧTCTL model checking to the untimed case. © Springer-Verlag Berlin Heidelberg 2005.

Año de publicación:

2005

Keywords:

• Dense real-time
• Formal Methods
• Model checking
• Multi-valued logic

Fuente:

scopus