nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Tableaux with Partial Caching for Hybrid PDL with Satisfaction Statements

verfasst von : Agathoklis Kritsimallis

Erschienen in: Theoretical Aspects of Computing – ICTAC 2017

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We give a novel deterministic tableau-based satisfiability algorithm for Hybrid Propositional Dynamic Logic (i.e. PDL with nominals) with satisfaction statements (\(\texttt {HPDL}_@\)). It builds and-or graphs in which it detects unfulfilled eventualities and unifies nodes (due to nominals) on-the-fly. There are two kinds of nodes: sentential nodes that represent partial descriptions of worlds of a model and unification nodes that deal with nominals. The main technical achievement of this work is the determination of the necessary information that a sentential node should have so that caching is feasible. Each saturated sentential node is available for reuse until it becomes out of date, due to loop dependencies. Thus, the algorithm runs in double exponential time. However, for iteration-free formulas, loops do not occur and thus, it works in exponential time. Nevertheless, despite the iteration operator, thanks to partial caching, the algorithm has the potential to achieve acceptable performance.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Constructing Cycles in the Simplex Method for DPLL(T)

Nächstes Kapitel PTrie: Data Structure for Compressing and Storing Sets via Prefix Sharing

The procedure calls backwEdge \((G,v_0,t,v_1)\) and cyclEdge \((G,v_0,t,v_1)\) define a backward and a cyclic edge \((v_0,v_1)\) (labelled with t), respectively. The procedure call addNode \((G,v_0,t,v_1)\) extends G with \(v_1\) (i.e. \(V := V \cup \{v_1\}\)) and if \(v_0\ne \bot \), then it defines the forward edge \((v_0,v_1)\) (i.e. \(E_f := E_f \cup \{(v_0,v_1)\}\)) and labels it with t.

Areces, C., Blackburn, P., Marx, M.: The computational complexity of hybrid temporal logics. Logic J. IGPL 8(5), 653–679 (2000)MathSciNetCrossRefMATH

Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Benthem, J.V., Wolter, F. (eds.) Handbook of Modal Logic, pp. 821–868. Elsevier, Amsterdam (2007)CrossRef

Bolander, T., Blackburn, P.: Termination for hybrid tableaus. J. Logic Comput. 17(3), 517–554 (2007)MathSciNetCrossRefMATH

Braüner, T.: Hybrid Logic and its Proof-Theory. Springer, Heidelberg (2011). doi:10.1007/978-94-007-0002-4 CrossRefMATH

Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)MathSciNetCrossRefMATH

Giacomo, G.D., Massacci, F.: Combining deduction and model checking into tableaux and algorithms for converse-PDL. Inf. Comput. 162, 117–137 (2000)MathSciNetCrossRefMATH

Goré, R.: And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 26–45. Springer, Cham (2014). doi:10.1007/978-3-319-08587-6_3

Goré, R., Kupke, C., Pattinson, D., Schröder, L.: Global caching for coalgebraic description logics. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 46–60. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14203-1_5 CrossRef

Goré, R., Nguyen, L.A.: Exptime tableaux for ALC using sound global caching. J. Autom. Reason. 50(4), 355–381 (2013)MathSciNetCrossRefMATH

10.

Goré, R., Widmann, F.: An optimal on-the-fly tableau-based decision procedure for PDL-satisfiability. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 437–452. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02959-2_32 CrossRef

11.

Goré, R., Widmann, F.: Optimal and cut-free tableaux for propositional dynamic logic with converse. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 225–239. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14203-1_20 CrossRef

12.

Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)MATH

13.

Hoffmann, G.: Lightweight hybrid tableaux. J. Appl. Log. 8(4), 397–408 (2010)MathSciNetCrossRefMATH

14.

Kaminski, M., Schneider, T., Smolka, G.: Correctness and worst-case optimality of Pratt-style decision procedures for modal and hybrid logics. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 196–210. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22119-4_16 CrossRef

15.

Kaminski, M., Smolka, G.: A goal-directed decision procedure for hybrid PDL. J. Autom. Reason. 52(4), 407–450 (2014)MathSciNetCrossRefMATH

16.

Kritsimallis, A.: Tableaux with partial caching for hybrid PDL with satisfaction statements (ext. ver.) (2017). https://www.academia.edu/32581641/Tableaux_with_Partial_Caching_for_Hybrid_PDL_with_Satisfaction_Statements

17.

Nguyen, L.A.: Exptime tableaux with global state caching for the description logic SHIO. Neurocomputing 146, 249–263 (2014)CrossRef

18.

Nguyen, L.A., Golińska-Pilarek, J.: An exptime tableau method for dealing with nominals and qualified number restrictions in deciding the description logic SHOQ. Fundamenta Informaticae 135(4), 433–449 (2014)MathSciNetMATH

19.

Nguyen, L.A., Szałas, A.: An optimal tableau decision procedure for converse-PDL. In: KSE 2009, pp. 207–214. IEEE (2009)

20.

Passy, S., Tinchev, T.: PDL with data constants. Inf. Process. Lett. 20, 35–41 (1985)MathSciNetCrossRefMATH

21.

Passy, S., Tinchev, T.: An essay in combinatory dynamic logic. Inf. Comput. 93(2), 263–332 (1991)MathSciNetCrossRefMATH

22.

Pratt, V.R.: Models of program logics. In: Proceedings of 20th Symposium on Foundations of Computer Science, pp. 115–122. IEEE (1979)

23.

Pratt, V.R.: A near-optimal method for reasoning about action. J. Comput. Syst. Sci. 20(2), 231–254 (1980)MathSciNetCrossRefMATH

24.

Prior, A.: Past, Present and Future. Oxford University Press, Oxford (1967)CrossRefMATH

25.

Tzakova, M.: Tableau calculi for hybrid logics. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS, vol. 1617, pp. 278–292. Springer, Heidelberg (1999). doi:10.1007/3-540-48754-9_24 CrossRef

Titel: Tableaux with Partial Caching for Hybrid PDL with Satisfaction Statements
verfasst von: Agathoklis Kritsimallis
Verlag: Springer International Publishing
Buch: Theoretical Aspects of Computing – ICTAC 2017
Print ISBN: 978-3-319-67728-6

Electronic ISBN: 978-3-319-67729-3

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-67729-3_14

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"