Sciweavers

Share
DLOG
2006

Model checking the basic modalities of CTL with Description Logic

9 years 21 days ago
Model checking the basic modalities of CTL with Description Logic
Abstract. Model checking is a fully automated technique for determining whether the behaviour of a finite-state reactive system satisfies a temporal logic specification. Despite the fact that model checking may require analyzing the entire reachable state space of a protocol under analysis, model checkers are routinely used in the computer industry. To allow for the analysis of large systems, different approaches to model checking have been developed, each approach allowing for a different class of systems to be analyzed. For instance, some model checkers represent program state spaces and transitions explicitly, others express these concepts implicitly. The determination of which flavour best suits a particular model must often be left to experimentation. Description Logic (DL) reasoners are capable of performing subsumption checks on large terminologies. In this paper, we show how to perform explicit state model checking with a DL reasoner. We formulate the check that a reactive syst...
Shoham Ben-David, Richard J. Trefler, Grant E. Wed
Added 30 Oct 2010
Updated 30 Oct 2010
Type Conference
Year 2006
Where DLOG
Authors Shoham Ben-David, Richard J. Trefler, Grant E. Weddell
Comments (0)
books