Abstract
When a protocol specified within a given system fails to ensure some desired properties, it is important to identify the actual causes of this failure. In this paper, we utilize a formal model of causal analysis in the situation calculus to show how one can specify the actual causes of such violations in non-deterministic protocols defined within dynamic systems. We show that our definition has some desirable properties.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)
Batusov, V., Soutchanski, M.: Situation calculus semantics for actual causality. In: Proceedings of AAAI Conference on Artificial Intelligence, pp. 1744–1752 (2018)
Claßen, J., Lakemeyer, G.: On the verification of very expressive temporal properties of non-terminating Golog programs. In: Proceedings of ECAI, pp. 887–892 (2010)
Datta, A., Garg, D., Kaynar, D.K., Sharma, D., Sinha, A.: Program actions as actual causes: a building block for accountability. In: Proceedings of IEEE Computer Security Foundations Symposium (CSF), pp. 261–275 (2015)
De Giacomo, G., Lespérance, Y., Levesque, H.J.: ConGolog, a concurrent programming language based on the situation calculus. Artif. Intell. 121(1–2), 109–169 (2000)
De Giacomo, G., Lespérance, Y., Patrizi, F., Sardiña, S.: Verifying ConGolog programs on bounded situation calculus theories. In: Proceedings of AAAI Conference on Artificial Intelligence, pp. 950–956 (2016)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Khan, S.M., Soutchanski, M.: Diagnosis as computing causal chains from event traces. In: Proceedings of AAAI Fall Symposium on Integrating Planning, Diagnosis, and Causal Reasoning (2018)
Leitner-Fischer, F., Leue, S.: Causality checking for complex system models. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 248–267. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35873-9_16
Liu, Y.: A hoare-style proof system for robot programs. In: Proceedings of AAAI/IAAI, pp. 74–79 (2002)
Mo, P., Li, N., Liu, Y.: Automatic verification of Golog programs via predicate abstraction. In: Proceedings of ECAI, pp. 760–768 (2016)
Reiter, R.: Knowledge in Action. Logical Foundations for Specifying and Implementing Dynamical Systems. MIT Press, Cambridge (2001)
Acknowledgement
This work was supported in part by the NSERC Canada.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Khan, S.M., Soutchanski, M. (2019). Towards Causal Analysis of Protocol Violations. In: Meurs, MJ., Rudzicz, F. (eds) Advances in Artificial Intelligence. Canadian AI 2019. Lecture Notes in Computer Science(), vol 11489. Springer, Cham. https://doi.org/10.1007/978-3-030-18305-9_30
Download citation
DOI: https://doi.org/10.1007/978-3-030-18305-9_30
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-18304-2
Online ISBN: 978-3-030-18305-9
eBook Packages: Computer ScienceComputer Science (R0)