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.
Chapter PDF
Similar content being viewed by others
References
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
Reiter, R.: Knowledge in action: logical foundations for describingand implementing dynamical systems. MIT Press, Cambridge (2001)
Giacomo, G.D., Ternovskaia, E., Reiter, R.: Non-terminating processes in the situation calculus. In: Proceedings of the AAAI 1997 Workshop on Robots, Softwoods, Immobots: Theories of Action, Planning and Control (1997)
Claβen, J., Lakemeyer, G.: A Logic for non-terminating Golog programs. In: Proceedings KR 2008, pp. 589–599. AAAI Press (2008)
Baader, F., Liu, H.K.: ul Mehdi, A.: Verifying properties of infinite sequences of description logic actions. In: Proceedings of ECAI 2010 (2010)
Baader, F., Ghilardi, S., Lutz, C.: LTL over description logic axioms. In: Proceedings of KR 2008, pp. 684–694. AAAI Press, Cambridge (2008)
Baader, F., Lutz, C., Sattler, U., Wolter, F.: Integrating description logics and action formalisms: First results. In: Proceedings AAAI 2005 (2005)
Chang, L., Shi, Z.Z., Gu, T.L., Zhao, L.: A family of dynamic description logics for representing and reasoning about actions. Journal of Automated Reasoning 49(1), 19–70 (2012)
Baader, F., Bauer, A., Lippmann, M.: Runtime verification using a temporal description logic. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 149–164. Springer, Heidelberg (2009)
Baader, F., Liu, H.K.: Intergrate Action Formalisms into Linear Temporal Description Logic. LTCS-Report 09-03, TU Dresden, Germany (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Wang, Y., Chang, L., Li, F., Gu, T. (2014). Verification of Branch-Time Property Based on Dynamic Description Logic. In: Shi, Z., Wu, Z., Leake, D., Sattler, U. (eds) Intelligent Information Processing VII. IIP 2014. IFIP Advances in Information and Communication Technology, vol 432. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44980-6_18
Download citation
DOI: https://doi.org/10.1007/978-3-662-44980-6_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44979-0
Online ISBN: 978-3-662-44980-6
eBook Packages: Computer ScienceComputer Science (R0)