SymbolicModelCheckingforConverse Propositional Dynamic Logicbased Industry 4.0
DOI:
https://doi.org/10.61841/8jjk6r75Keywords:
model checking, : Converse propositional dynamic logic(CPDL), Ordered Binary Decision Diagram (OBDD)Abstract
Propositional Dynamic Logic with Converse (CPDL) is a modal logic developed for reasoning about programs with applications for instance in knowledge representation. This paper presents a symbol model checking algorithm for propositional dynamic logic with converse. First of all, according to the analysis of symbolic model checking technology by ordered binary decision diagram, we describe how to represent propositional dynamic logic with converse model system symbolically using ordered binary decision diagram. Then a symbolic model checking algorithm for propositional dynamic logic with converse is proposed. Finally, the proof of the algorithm is given, and the validity of this algorithm was verified by an example.
Downloads
References
[1] D. Harel, D. Kozen and J. Tiuryn.(2000). Dynamic Logic, MIT Press, Cambridge, MA.
[2] M. Fischer and R.Ladner. (1979). Propositional dynamic logic of regular programs.Journal of Computer and System Sciences, 18(2):194-211.
[3] C.Lutz. (2005).PDL with Intersection and Converse is Decidable.In Annual Conference of the
European Association for Computer Science Logic CSL'05, LNCS. Springer Verlag.
[4] Stefan Göller, Markus Lohrey, Carsten Lutz.(2007). PDL with Intersection and Converse is 2EXP-complete. Algorithmic-Logical Theory of Infinite Structures.
[5] Benevides, Mario R. F.(2008). A propositional dynamic logic for CCS programs.In15th International Workshop on Logic, Language, Information and Computation, Springer Verlag
[6] Fahima Cheikh, Giuseppe De Giacomo.(2006).
Automatic Web Services Composition in Trust-aware Communities. ACM
[7] J.C. Meyer, Dynamic logic reasoning about actions and agents.(1999). In Proc. Workshop on Logic-Based Arti-ficial Intelligence, Washington, DC, USA
[8] L. Spalazzi, P. Traverso. (2000). A dynamic logic for acting, sensing, and planning, J. Logic Comput. 10 (6): 787–821
[9] F. van Harmelen, J. Balder.(1992). A formal language for KADS models of expertise.Knowledge Acqui-sition 4: 127–161
[10] H.P. van Ditmarsch, W. van der Hoek, B.P. Kooi. (2003). Concurrent dynamic epistemic logic for MAS. In Proc.2nd Int. Joint Conference on Autonomous Agents and Multiagent Systems, Melbourne,
Australia, ACM Press, pages 201–208
[11] G.D. Giacomo, M. Lenzerini.(1994). Boosting the correspondence between description logics and propositional dynamic logics. In Proc. of the 12th National Conference on Artificial Intelligence, AAAI’94, AAAI Press/MIT Press, pages 205–212.
[12] GiuseppeDeGiacomo,Fabio Massacci. (2000) .Combining Deduction and Model Checking into Tableaux and Algorithms for Converse-PDL. Inf. Comput. 162(1-2): 117-137.
[13] M. Lange. (2006). Modelchecking propositional dynamic logic with all extras. Journal of Applied Logic, 4:39-49.
[14] Bryant R. (1986).Graph-Base Algorithm for Boolean Function Manipulation.Transactions on computer , pages 677-691
[15] BRYANT R E. (1992). Symbolic Boolean manipulation with ordered binarydecision diagrams. ACM Computing Surveys,124 (3):293-318
[16] E. Clarke, Orna Grumberg and D. Peled.(2000) Model Checking,MIT Press
[17] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J.(1990). Hwang. Symbolic model checking: 1020 states and beyond. In Proc. Symposium on Logic in Computer Science, pages 428–439. IEEE.
[18] Stefan Göller, Markus Lohrey, and Carsten Lutz. (2009).PDL with intersection and converse: satisfiability and infinite-state model checking. Volume 74, pages. 279-314.
[19] B. Yang, R. E. Bryant, D. R. O’Hallaron, A. Biere, O. Coudert, G. Janssen, R. K. Ranjan & F. Somenzi.(1998).A Performance Study of BDD-Based Model Checking. InProceedings of the Second International Conference on Formal Methods in Computer-Aided Design, FMCAD ’98, Springer Verlag, London, UK, pages. 255–289.
[20] A Goel, G. Hasteer & R. Bryant.(2003).Symbolic representation with ordered function templates.
InProceedings of the 40th annual Design Automation Conference
[21] Christian Doczkal, Joachim Bard (2018) Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
[22] Sedla´r, I. (2016).Non-classical PDL on the cheap. Manuscript.
[23] Teheux, B. (2014). Propositional dynamic logic for searching games with errors. Journal of Applied Logic 12(4), 377–394
Downloads
Published
Issue
Section
License
This work is licensed under a Creative Commons Attribution 4.0 International License.
You are free to:
- Share — copy and redistribute the material in any medium or format for any purpose, even commercially.
- Adapt — remix, transform, and build upon the material for any purpose, even commercially.
- The licensor cannot revoke these freedoms as long as you follow the license terms.
Under the following terms:
- Attribution — You must give appropriate credit , provide a link to the license, and indicate if changes were made . You may do so in any reasonable manner, but not in any way that suggests the licensor endorses you or your use.
- No additional restrictions — You may not apply legal terms or technological measures that legally restrict others from doing anything the license permits.
Notices:
You do not have to comply with the license for elements of the material in the public domain or where your use is permitted by an applicable exception or limitation .
No warranties are given. The license may not give you all of the permissions necessary for your intended use. For example, other rights such as publicity, privacy, or moral rights may limit how you use the material.
