×

Probabilization of logics: completeness and decidability. (English) Zbl 1323.03033

Summary: The probabilization of a logic system consists of enriching the language (the formulas) and the semantics (the models) with probabilistic features. Such an operation is said to be exogenous if the enrichment is done on top, without internal changes to the structure, and is called endogenous otherwise. These two different enrichments can be applied simultaneously to the language and semantics of a same logic. We address the problem of studying the transference of metaproperties, such as completeness and decidability, to the exogenous probabilization of an abstract logic system. First, we setup the necessary framework to handle the probabilization of a satisfaction system by proving transference results within a more general context. In this setup, we define a combination mechanism of logics through morphisms and prove sufficient condition to guarantee completeness and decidability. Then, we demonstrate that probabilization is a special case of this exogenous combination method, and that it fulfills the general conditions to obtain transference of completeness and decidability. Finally, we motivate the applicability of our technique by analyzing the probabilization of the linear temporal logic over Markov chains, which constitutes an endogenous probabilization. The results are obtained first by studying the exogenous semantics, and then by establishing an equivalence with the original probabilization given by Markov chains.

MSC:

03B62 Combined logics
03B48 Probability and inductive logic
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aziz, A., Singhal, V., Balarin, F.: It usually works: the temporal logic of stochastic systems. In: Proceedings of the 7th International Conference on Computer Aided Verification, pp. 155–165. Springer, London (1995)
[2] Baier C., Kwiatkowska M.Z.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11(3), 125–155 (1998) · doi:10.1007/s004460050046
[3] Baltazar P., Chadha R., Mateus P.: Quantum computation tree logic–model checking and complete calculus. Int. J. Quantum Inf. 6(2), 281–302 (2008) · Zbl 1151.81305 · doi:10.1142/S0219749908003530
[4] Baltazar, P., Mateus, P.: Temporalization of probabilistic propositional logic. In: Artemov, S., Nerode, A. (eds.) LFCS’09: Proceedings of the 2009 International Symposium on Logical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 5407, pp. 46–60. Springer, Berlin (2009) · Zbl 1211.03042
[5] Barwise K.J.: Axioms for abstract model theory. Ann. Math. Logic. 7(2–3), 221–265 (1974) · Zbl 0324.02034 · doi:10.1016/0003-4843(74)90016-3
[6] Blackburn P., de Rijke M., Venema Y.: Modal Logic. Cambridge University Press, London (2001) · Zbl 0988.03006
[7] Boole G.: An Investigation of the Laws of Thought on Which are Founded the Mathematical Theories of Logic and Probabilities. Walton, London (1854) · Zbl 1205.03003
[8] Caleiro, C., Mateus, P., Sernadas, A., Sernadas, C.: Quantum institutions. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation–Essays Dedicated to Joseph Goguen. LNCS, vol. 4060, pp. 50–64. Springer, Berlin (2006) · Zbl 1132.03354
[9] Caleiro, C., Sernadas, C., Sernadas, A.: Parameterisation of logics. In: Fiadeiro, J. (ed.) Recent Trends in Algebraic Development Techniques–Selected Papers. Lecture Notes in Computer Science, vol. 1589, pp. 48–62. Springer, Berlin (1999) · Zbl 0943.03007
[10] Canny, J.: Some algebraic and geometric computations in pspace. In: Stoc ’88: Proceedings of the Twentieth Annual ACM Symposium on Theory Of Computing, pp. 460–469. ACM, New York (1988).
[11] Carnap R.: Logical Foundations of Probability. Routledge and Kegan Paul, London (1951) · Zbl 0044.00107
[12] Carnielli, W.A., Coniglio, M.E., Gabbay, D., Gouveia, P., Sernadas, C.: Analysis and Synthesis of Logics–How To Cut And Paste Reasoning Systems. Applied Logic, vol. 35. Springer, Berlin (2008) · Zbl 1137.03001
[13] Chvátal V.: Linear Programming. Freeman, San Francisco (1983) · Zbl 0537.90067
[14] Cleaveland R., Iyer S.P., Narasimha M.: Probabilistic temporal logics via the modal mu-calculus. Theor. Comput. Sci. 342(2–3), 316–350 (2005) · Zbl 1077.68058 · doi:10.1016/j.tcs.2005.03.048
[15] Cruz-Filipe L., Rasga J., Sernadas A., Sernadas C.: A complete axiomatization of discrete-measure almost-everywhere quantification. J. Log. Comput. 18(6), 885–911 (2008) · Zbl 1157.03014 · doi:10.1093/logcom/exn014
[16] Ehrich H.-D.: On the theory of specification, implementation, and parametrization of abstract data types. J. ACM. 29(1), 206–227 (1982) · Zbl 0478.68020 · doi:10.1145/322290.322303
[17] Fagin R., Halpern J., Megiddo N.: A logic for reasoning about probabilities. Inf. Comput. 87(1/2), 78–128 (1990) · Zbl 0811.03014 · doi:10.1016/0890-5401(90)90060-U
[18] Finger, M., Gabbay, D.M.: Adding a temporal dimension to a logic system. J. Log. Lang. Inf. 1(3): 203–233, 09 (1992) · Zbl 0798.03031
[19] Goguen, J., Rosu, G.: Institution morphisms. Form. Asp. Comput. 13(3–5), 274–307 (2002) (special issue in honor of the retirement of Rod Burstall) · Zbl 1001.68019
[20] Goguen, J.A., Burstall, R.M.: Introducing institutions. In:Proceedings of the Carnegie Mellon Workshop on Logic of Programs. pp. 221–256. Springer, London (1984) · Zbl 0543.68021
[21] Halpern, J.Y.: An analysis of first-order logics of probability. In: IJCAI’89: Proceedings of the 11th International Joint Conference on Artificial intelligence, pp. 1375–1381. Morgan Kaufmann Publishers Inc., San Francisco (1989)
[22] Halpern J.Y.: Reasoning About Uncertainty. MIT Press, Cambridge (2003) · Zbl 1090.68105
[23] Hasson H., Jonsson B.: A logic for reasoning about time and probability. Form. Asp. Comput. 6, 512–535 (1994) · Zbl 0820.68113 · doi:10.1007/BF01211866
[24] Henriques D., Biscaia M., Baltazar P., Mateus P.: Decidability and complexity for omega-regular properties of stochastic systems. Log. J. IGPL. 20(6), 1175–1201 (2012) · Zbl 1277.68218 · doi:10.1093/jigpal/jzr054
[25] Kolmogorov, A.N.: Grundbegriffe der Wahrscheinlichkeitsrechnung. Berlin (1933) (Second English Edition, Foundations of Probability 1950, published by Chelsea, New York) · JFM 59.1154.01
[26] Kozen D.: A probabilistic PDL. J. Comput. Syst. Sci. 30, 162–178 (1985) · Zbl 0575.03013 · doi:10.1016/0022-0000(85)90012-1
[27] Legay, A., Murawski, A., Ouaknine, J., Worrell, J.: On automated verification of probabilistic programs. In: Ramakrishnan, C., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963, pp. 173–187. Springer, Berlin (2008)
[28] Mateus P., Sernadas A.: Weakly complete axiomatization of exogenous quantum propositional logic. Inf. Comput. 204(5), 771–794 (2006) · Zbl 1116.03021 · doi:10.1016/j.ic.2006.02.001
[29] Mateus, P., Sernadas, A., Sernadas, C.: Exogenous semantics approach to enriching logics. In: Sica, G. (ed.) Essays on the Foundations of Mathematics and Logic, vol. 1, pp. 165–194. Polimetrica, Italy (2005) · Zbl 1151.03324
[30] Ng R., Subrahmanian V.S.: Probabilistic logic programming. Inf. Comput. 101(2), 150–201 (1992) · Zbl 0781.68038 · doi:10.1016/0890-5401(92)90061-J
[31] Nilsson N.J.: Probabilistic logic. Artif. Intell. 28, 71–87 (1986) · Zbl 0589.03007 · doi:10.1016/0004-3702(86)90031-7
[32] Ognjanović Z.: Discrete linear-time probabilistic logics: completeness, decidability and complexity. J. Log. Comput. 16(2), 257–285 (2006) · Zbl 1102.03022 · doi:10.1093/logcom/exi077
[33] Port S.C.: Theoretical Probability for Applications. Wiley, New York (1993) · Zbl 0860.60001
[34] Rasga J., Sernadas A., Sernadas C.: Importing logics. Stud. Log. 100(3), 545–581 (2012) · Zbl 1280.03033 · doi:10.1007/s11225-012-9414-y
[35] Roeper P., Leblanc H.: Probability Theory and Probability Logic. University of Toronto Press, Toronto (1999) · Zbl 0931.03037
[36] Rybakov V.V.: Admissibility of Logical Inference Rules. Elsevier Science Pub, Amsterdam (1997) · Zbl 0872.03002
[37] Sernadas A., Sernadas C., Caleiro C.: Synchronization of logics. Stud. Log. 59(2), 217–247 (1997) · Zbl 0882.03008 · doi:10.1023/A:1004904401346
[38] Sernadas A., Sernadas C., Caleiro C.: Fibring of logics as a categorial construction. J. Log. Comput. 9(2), 149–179 (1999) · Zbl 0942.03064 · doi:10.1093/logcom/9.2.149
[39] Sharir M., Pnueli A., Hart S.: Verification of probabilistic programs. SIAM J. Comput. 13(2), 292–314 (1984) · Zbl 0533.68012 · doi:10.1137/0213021
[40] Tarski, A.: A decision method for elementary algebra and geometry. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 24–84. Springer, Vienna (1998) · Zbl 0900.03045
[41] Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st Symposium on Logic in Computer Science, Cambridge, pp. 332–344 (1986)
[42] Vardi M.Y., Wolper P.: Reasoning about infinite computations. Inf. Comput. 115, 1–37 (1994) · Zbl 0827.03009 · doi:10.1006/inco.1994.1092
[43] Zhou C.: A complete deductive system for probability logic. J. Log. Comput. 19(6), 1427–1454 (2009) · Zbl 1191.03018 · doi:10.1093/logcom/exp031
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.