×

Enhancing probabilistic model checking with ontologies. (English) Zbl 1522.68310

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68T27 Logic in artificial intelligence
68T30 Knowledge representation
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baader F, Brandt S, Lutz C (2005) Pushing the \(\cal EL\it\) envelope. In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence IJCAI-05, Edinburgh, UK, Morgan-Kaufmann Publishers
[2] Baier, C.; Chrszon, P.; Dubslaff, C.; Klein, J.; Klüppelholz, S., Energy-utility analysis of probabilistic systems with exogenous coordination, It’s All About Coordination, 38-56 (2018), Cham: LNCS. Springer, Cham · doi:10.1007/978-3-319-90089-6_3
[3] Baader F, Calvanese D, McGuinness DL, Nardi D, Patel-Schneider PF (eds) (2003) The description logic handbook: theory, implementation, and applications. Cambridge University Press · Zbl 1058.68107
[4] Baier C, Daum M, Dubslaff C, Klein J, Klüppelholz S (2014) Energy-utility quantiles. In: Proc. NASA Formal Methods (NFM’14), volume 8430 of LNCS, pages 285-299. Springer
[5] Baier, C.; Dubslaff, C.; Klüppelholz, S.; Daum, M.; Klein, J.; Märcker, S.; Wunderlich, S., Probabilistic model checking and non-standard multi-objective reasoning, Fundamental Approaches to Software Engineering, 1-16 (2014), Berlin, Heidelberg: Springer, Berlin, Heidelberg
[6] Baader F, Philipp H (1991) A scheme for integrating concrete domains into concept languages. In: Proceedings of IJCAI 1991. Morgan Kaufmann, pp 452-457 · Zbl 0742.68063
[7] Baader, F.; Horrocks, I.; Lutz, C.; Sattler, U., An introduction to description logic (2017), Cambridge University Press · Zbl 1373.68002 · doi:10.1017/9781139025355
[8] Baier, C.; Katoen, J-P, Principles of model checking (2008), MIT Press · Zbl 1179.68076
[9] Baader F, Koopmann P, Turhan A-Y (2017) Using ontologies to query probabilistic numerical data. In: Frontiers of Combining Systems: 11th International Symposium, volume 10483 of LNCS. Springer International Publishing, pp 77-94 · Zbl 1495.68216
[10] Bienvenu M, Ortiz M (2015) Ontology-mediated query answering with data-tractable description logics. In: Reasoning Web. Web Logic Rules, pp 218-307 · Zbl 1358.68086
[11] Baader F, Peñaloza R, Suntisrivaraporn B (2007) Pinpointing in the description logic \({{\cal EL\it }^+}\). In: Proceedings of the 30th German Annual Conference on Artificial Intelligence (KI’07), volume 4667 of Lecture Notes in Computer Science. Springer, Osnabrück, Germany, pp 52-67
[12] Brandt S (2004) Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and—what else? In: López de Mantáras R, Saitta L, editors, Proceedings of the 16th European Conference on Artificial Intelligence (ECAI-2004), pages 298-302. IOS Press
[13] Brayton, RK; Sangiovanni-Vincentelli, AL; McMullen, CT; Hachtel, GD, Logic minimization algorithms for VLSI synthesis (1984), USA: Kluwer Academic Publishers, USA · Zbl 0565.94020 · doi:10.1007/978-1-4613-2821-6
[14] Baader F, Zarrieß B (2013) Verification of Golog programs over description logic actions. In: Proceedings of FroCos 2013, volume 8152 of LNCS. Springer, pp 181-196 · Zbl 1398.68568
[15] Chrszon P, Baier C, Dubslaff C, Klüppelholz S (2020) From features to roles. In: Proceedings of the 24th ACM Conference on Systems and Software Product Line: Volume A, SPLC ’20, New York, NY, USA. Association for Computing Machinery
[16] Chrszon, P.; Dubslaff, C.; Baier, C.; Klein, J.; Klüppelholz, S., Modeling role-based systems with exogenous coordination, 122-139 (2016), Cham: Springer, Cham · Zbl 1475.68077
[17] Calvanese D, De Giacomo G, Lenzerini M, Rosati R (2011) Actions and programs over description logic knowledge bases: a functional approach. In: Knowing, reasoning, and acting: essays in honour of H. J. Levesque. College Publications · Zbl 1341.68222
[18] Chrszon, P.; Dubslaff, C.; Klüppelholz, S.; Baier, C., Profeat: feature-oriented engineering for family-based probabilistic model checking, Formal Aspects Comput, 30, 1, 45-75 (2018) · doi:10.1007/s00165-017-0432-4
[19] Calvanese, D.; De Giacomo, G.; Lembo, D.; Lenzerini, M.; Rosati, R., Tractable reasoning and efficient query answering in description logics: the DL-Lite family, J Autom Reason, 39, 3, 385-429 (2007) · Zbl 1132.68725 · doi:10.1007/s10817-007-9078-x
[20] Dubslaff, C.; Baier, C.; Klüppelholz, S., Probabilistic model checking for feature-oriented systems, Trans Aspect-Orient Softw Dev, 12, 180-220 (2015)
[21] Dhaussy, P.; Boniol, F.; Roger, J-C; Leroux, L., Improving model checking with context modelling, Adv Softw Eng, 2012, 13 (2012) · doi:10.1155/2012/547157
[22] Dijkstra, EW, A discipline of programming (1976), Prentice-Hall · Zbl 0368.68005
[23] Dehnert C, Junges S, Katoen J-P, Volk M (2017) A storm is coming: a modern probabilistic model checker. In: 29th International Conference on Computer Aided Verification (CAV), volume 10427 of LNCS. Springer, pp 592-600
[24] Dubslaff, C.; Koopmann, P.; Turhan, A-Y; Ahrendt, W.; Tarifa, SLT, Ontology-mediated probabilistic model checking, Integrated formal methods-15th International Conference, IFM 2019, 194-211 (2019), Springer
[25] Dubslaff C, Koopmann P, Turhan A-Y (2020) Give inconsistency a chance: Semantics for ontology-mediated verification. In: Proceedings of the 33rd International Workshop on Description Logics
[26] Forejt V, Kwiatkowska MZ, Norman G, Parker D (2011) Automated verification techniques for probabilistic systems. In: Proceedings of the School on Formal Methods for the Design of Computer, Communication and Software Systems, Formal Methods for Eternal Networked Software Systems (SFM’11), volume 6659 of LNCS. Springer, pp 53-113 · Zbl 1315.68177
[27] Glimm, B.; Horrocks, I.; Motik, B.; Stoilos, G.; Wang, Z., HermiT: an OWL 2 reasoner, J Autom Reason, 53, 3, 245-269 (2014) · Zbl 1314.68280 · doi:10.1007/s10817-014-9305-1
[28] Horridge, M.; Bechhofer, S., The OWL API: a Java API for OWL ontologies, Semantic Web, 2, 1, 11-21 (2011) · doi:10.3233/SW-2011-0025
[29] Hariri, BB; Calvanese, D.; Montali, M.; De Giacomo, G.; De Masellis, R.; Felli, P., Description logic knowledge and action bases, J Artif Intell Res, 46, 651-686 (2013) · Zbl 1280.68249 · doi:10.1613/jair.3826
[30] Hirschfeld, R.; Costanza, P.; Nierstrasz, O., Context-oriented programming. J Object Technol, 7, 3, 125-151 (2008)
[31] Horrocks I, Kutz O, Sattler U (2006) The even more irresistible \(\cal SROIQ\it \). In: Proceedings of KR 2006. AAAI Press, pp 57-67
[32] Horridge M (2011) Justification based explanation in ontologies. PhD thesis, University of Manchester, UK
[33] Jifeng, H.; Seidel, K.; McIver, A., Probabilistic models for the guarded command language, Sci Comput Programm, 28, 2, 171-192 (1997) · Zbl 0877.68014 · doi:10.1016/S0167-6423(96)00019-6
[34] Kazakov \(Y (2008) \cal RIQ\it\) and \(\cal SROIQ\it\) are harder than \(\cal SHOIQ\it \). In: Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR’08). AAAI Press, pp 274-284
[35] Klein, J.; Baier, C.; Chrszon, P.; Daum, M.; Dubslaff, C.; Klüppelholz, S.; Märcker, S.; Müller, D., Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic büchi automata, Int J Softw Tools Technol Transf, 20, 2, 179-194 (2018) · doi:10.1007/s10009-017-0456-3
[36] Kühn T, Böhme S, Götz S, Aßmann U (2015) A combined formal model for relational context-dependent roles. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Software Language Engineering, SLE 2015, Pittsburgh, PA, USA, October 25-27, 2015, pp 113-124
[37] Kazakov, Y.; Krötzsch, M.; Simancik, F., The incredible ELK - from polynomial procedures to efficient reasoning with \(\cal{EL}\) ontologies, J Autom Reason, 53, 1, 1-61 (2014) · Zbl 1331.68216 · doi:10.1007/s10817-013-9296-3
[38] Kwiatkowska MZ, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11), volume 6806 of LNCS, pp 585-591
[39] Kalyanpur, A.; Parsia, B.; Horridge, M.; Sirin, E.; Aberer, K.; Choi, K-S; Noy, NF; Allemang, D.; Lee, K-I; Nixon Lyndon, JB; Golbeck, J.; Mika, P.; Maynard, D.; Mizoguchi, R.; Schreiber, G.; Cudré-Mauroux, P., Finding all justifications of OWL DL entailments, The Semantic Web, 6th International Semantic Web Conference, 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea, November 11-15, 2007, 267-280 (2007), Springer · doi:10.1007/978-3-540-76298-0_20
[40] Lutz C, Schröder L (2010) Probabilistic description logics for subjective uncertainty. In: Proceedings of the 12th international conference on principles of knowledge representation and reasoning (KR2010). AAAI Press · Zbl 1401.68305
[41] Lutz C (2007) Inverse roles make conjunctive queries hard. In: Proceedings of the 20th International workshop on description logics (DL’07), volume 250 of CEUR workshop proceedings. CEUR-WS.org
[42] Motik B, Cuenca Grau B, Horrocks I, Wu Z, Fokoue A, Lutz C, OWL 2 web ontology language profiles. W3C Recommendation, 27 Oct 2009. http://www.w3.org/TR/2009/REC-owl2-profiles-20091027/
[43] Mauro J, Nieke M, Seidl C, Yu IC (2016) Context aware reconfiguration in software product lines. In: Proceedings of the 10th international workshop on variability modelling of software-intensive systems (VaMoS’16). ACM, pp 41-48
[44] Miner AS,Parker D (2004) Symbolic representations and analysis of large probabilistic systems. In: Validation of Stochastic Systems - A Guide to Current Research, volume 2925 of LNCS, pages 296-338 · Zbl 1203.68117
[45] Ngo N, Ortiz M, Simkus M (2016) Closed predicates in description logics: results on combined complexity. In: Proceedings of KR 2016. AAAI Press, pp 237-246
[46] Poggi A, Lembo D, Calvanese D, De Giacomo G, Lenzerini M, Rosati R (2008) Linking data to ontologies. J Data Semant · Zbl 1132.68061
[47] Parsia, B.; Matentzoglu, N.; Gonçalves, RS; Glimm, B.; Steigmiller, A., The OWL reasoner evaluation (ORE) 2015 competition report, J Autom Reason, 59, 4, 455-482 (2017) · Zbl 1425.68402 · doi:10.1007/s10817-017-9406-8
[48] Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, Providence, Rhode Island, USA, 31 October-1 November 1977, pp 46-57
[49] Peñaloza R, Turhan A-Y (2013) Instance-based non-standard inferences in \(\cal EL\it\) with subjective probabilities. In: Uncertainty reasoning for the semantic web II, International Workshops, Revised Selected Papers, number 7123 in LNCS. Springer, pp 80-98 · Zbl 1351.68269
[50] Puterman, M., Markov decision processes: discrete stochastic dynamic programming (1994), New York, NY: Wiley, New York, NY · Zbl 0829.90134 · doi:10.1002/9780470316887
[51] Rudolph, S.; Glimm, B., Nominals, inverses, counting, and conjunctive queries or: why infinity is your friend!, J Artif Intell Res, 39, 429-481 (2010) · Zbl 1205.68408 · doi:10.1613/jair.3029
[52] Romero, AA; Kaminski, M.; Grau, BC; Horrocks, I., Module extraction in expressive ontology languages via datalog reasoning, J Artif Intell Res, 55, 499-564 (2016) · Zbl 1352.68235 · doi:10.1613/jair.4898
[53] Schlobach S, Cornet R (2003) Non-standard reasoning services for the debugging of description logic terminologies. In: Gottlob G, Walsh T (eds) Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI 2003), Acapulco, Mexico, Morgan Kaufmann, pp 355-362
[54] Schild, K.; John, M.; Raymond, R., A correspondence theory for terminological logics: preliminary report, Proc IJCAI’91, 466-471 (1991), Morgan Kaufmann · Zbl 0742.68059
[55] Steigmiller, A.; Liebig, T.; Glimm, B., Konclude: system description, J Web Semant, 27-28, 78-85 (2014) · doi:10.1016/j.websem.2014.06.003
[56] Sirin, E.; Parsia, B.; Grau, BC; Kalyanpur, A.; Katz, Y., Pellet: a practical OWL-DL reasoner, J Web Sem, 5, 2, 51-53 (2007) · doi:10.1016/j.websem.2007.03.004
[57] Tobies S (2001) Complexity results and practical algorithms for logics in knowledge representation. PhD thesis, RWTH Aachen University, Germany
[58] Vardi MY (1985) Automatic verification of probabilistic concurrent finite-state programs. In: 26th IEEE symposium on foundations of computer science (FOCS), pp 327-338. IEEE Computer Society
[59] Zarrieß B, Claßen J (2015) Verification of knowledge-based programs over description logic actions. In: IJCAI. AAAI Press, pp 3278-3284
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.