Verification of Branch-Time Property Based on Dynamic Description Logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

Verification of Branch-Time Property Based on Dynamic Description Logic

Yaoguang Wang
  • Fonction : Auteur
  • PersonId : 990786
Liang Chang
  • Fonction : Auteur
  • PersonId : 990787
Fengying Li
  • Fonction : Auteur
  • PersonId : 990788
Tianlong Gu
  • Fonction : Auteur
  • PersonId : 990789

Résumé

The dynamic description logic DDL provides formalism for describing dynamic system in the semantic Web environment Model checking is a formal verification method based on state transition system. In this paper, we bring dynamic description logic into model checking. Firstly, state transition systems considered in model checking are modeled as complex actions in dynamic description logic. Secondly, a kind of temporal description logic DL-CTL is introduced to specify temporal properties on state transition systems, where DL-CTL is a DL-based extension of propositional branch-time temporal logic CTL. Finally, verification algorithm is presented with the help of reasoning mechanisms provided by description logic.
Fichier principal
Vignette du fichier
978-3-662-44980-6_18_Chapter.pdf (631.72 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01383329 , version 1 (18-10-2016)

Licence

Paternité

Identifiants

Citer

Yaoguang Wang, Liang Chang, Fengying Li, Tianlong Gu. Verification of Branch-Time Property Based on Dynamic Description Logic. 8th International Conference on Intelligent Information Processing (IIP), Oct 2014, Hangzhou, China. pp.161-170, ⟨10.1007/978-3-662-44980-6_18⟩. ⟨hal-01383329⟩
57 Consultations
88 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More