| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Verification of Branch-Time Property Based on Dynamic Description Logic
Abstract : 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.
Cited literature [9 references]
https://hal.inria.fr/hal-01383329
Contributor : Hal Ifip <>
Submitted on : Tuesday, October 18, 2016 - 2:55:04 PM
Last modification on : Thursday, March 5, 2020 - 5:41:04 PM
Contributor : Hal Ifip <>
Submitted on : Tuesday, October 18, 2016 - 2:55:04 PM
Last modification on : Thursday, March 5, 2020 - 5:41:04 PM
File
978-3-662-44980-6_18_Chapter.p...
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution 4.0 International License