×

\(L\)-fuzzy strongest postcondition predicate transformers as \(L\)-idempotent linear or affine operators between semimodules of monotonic predicates. (English) Zbl 1252.68194

Summary: For a completely distributive quantale \(L\), \(L\)-fuzzy strongest postcondition predicate transformers are introduced, and it is shown that, under reasonable assumptions, they are linear or affine continuous mappings between continuous \(L\)-idempotent semimodules of \(L\)-fuzzy monotonic predicates.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing

References:

[1] Akian, M., Densities of invariant measures and large deviations, Trans. Am. Math. Soc., 351, 11, 4515-4543 (1999) · Zbl 0934.28005
[2] Bergmann, M., Introduction to Many-Valued and Fuzzy Logic: Semantics, Algebras, and Derivation Systems (2008), Cambridge University Press: Cambridge University Press New York · Zbl 1148.03001
[3] Y. Chen, H. Wu, Implication-based fuzzy predicate transformers, in: Fuzzy Logic, Soft Computing and Computational Intelligence: Eleventh International Fuzzy Systems Association, vol. I, Beijing, 2005, pp. 77-82.; Y. Chen, H. Wu, Implication-based fuzzy predicate transformers, in: Fuzzy Logic, Soft Computing and Computational Intelligence: Eleventh International Fuzzy Systems Association, vol. I, Beijing, 2005, pp. 77-82.
[4] Y. Chen, H. Wu, The semantics of wlp and slp of fuzzy imperative programming languages, in: Nonlinear Mathematics for Uncertainty and its Applications, Advances in Intelligent and Soft Computing, vol. 100, 2011, pp. 357-364.; Y. Chen, H. Wu, The semantics of wlp and slp of fuzzy imperative programming languages, in: Nonlinear Mathematics for Uncertainty and its Applications, Advances in Intelligent and Soft Computing, vol. 100, 2011, pp. 357-364. · Zbl 1267.68092
[5] J.T. Denniston, A. Melton, S.E. Rodabaugh, Lattice-valued predicate transformers and interchange systems, in: P. Cintula, E. P. Klement, L.N. Stout (Eds.), Abstracts of the 31st Linz Seminar (February 2010), Universitätsdirecktion Johannes Kepler Universität (Linz, Austria), pp. 31-40.; J.T. Denniston, A. Melton, S.E. Rodabaugh, Lattice-valued predicate transformers and interchange systems, in: P. Cintula, E. P. Klement, L.N. Stout (Eds.), Abstracts of the 31st Linz Seminar (February 2010), Universitätsdirecktion Johannes Kepler Universität (Linz, Austria), pp. 31-40.
[6] Dijkstra, E. W., Guarded commands, non-determinacy and formal derivation of programs, Commun. ACM, 18, 8, 453-457 (1975) · Zbl 0308.68017
[7] E.E. Doberkat, Demonic Product of Probabilistic Relations, Technical Report 116, University of Dortmund.; E.E. Doberkat, Demonic Product of Probabilistic Relations, Technical Report 116, University of Dortmund. · Zbl 1077.68715
[8] Dubois, D.; Prade, H., Gradualness, Uncertainty and Bipolarity: Making Sense of Fuzzy Sets, Fuzzy Sets and Systems, 192, 3-24 (2012) · Zbl 1238.03044
[9] Edalat, A., Domains for computation in mathematics, physics and exact real arithmetic, Bull. Symb. Logic, 3, 4, 401-452 (1997) · Zbl 0946.03055
[10] M. Erné, Z-Distributive Function Spaces, Preprint, 1998.; M. Erné, Z-Distributive Function Spaces, Preprint, 1998.
[11] Gierz, G.; Hofmann, K. H.; Keimel, K.; Lawson, J. D.; Mislove, M.; Scott, D. S., Continuous Lattices and Domains (2003), Cambridge University Press · Zbl 1088.06001
[12] Hájek, P., Fuzzy logics with noncommutative conjunctions, J. Logic Comput., 13, 4, 469-479 (2003) · Zbl 1036.03018
[13] R. Heckmann, M. Huth, A duality theory for quantitative semantics, in: Proceedings of the 11th International Workshop on Computer Science Logic, Lecture Notes in Computer Science, vol. 1414, Springer Verlag, 1998, pp. 255-274.; R. Heckmann, M. Huth, A duality theory for quantitative semantics, in: Proceedings of the 11th International Workshop on Computer Science Logic, Lecture Notes in Computer Science, vol. 1414, Springer Verlag, 1998, pp. 255-274. · Zbl 0908.06004
[14] Mac Lane, S., Categories for the Working Mathematician (1998), Springer: Springer New York · Zbl 0906.18001
[15] Ying, Mingsheng, Reasoning about probabilistic sequential programs in a probabilistic logic, Acta Inf., 39, 5, 315-389 (2003) · Zbl 1060.68073
[16] Morgan, C.; McIver, A.; Seidel, K., Probabilistic predicate transformers, ACM Trans. Program. Lang. Syst., 18, 3, 325-353 (1996)
[17] Nykyforchyn, O., Capacities with values in compact Hausdorff lattices, Appl. Cat. Struct., 15, 3, 243-257 (2007) · Zbl 1141.18004
[18] Nykyforchyn, O., Adjoints and monads related to compact lattices and compact Lawson idempotent semimodules, Order, 29, 1, 192-213 (2012) · Zbl 1259.06006
[19] Nykyforchyn, O., Continuous and dually continuous \(L\)-semimodules, Mat. Stud., 37, 1, 3-28 (2012) · Zbl 1305.46064
[20] K. Rosenthal, Quantales and Their Applications, Pitman Research Notes in Mathematics Series, vol. 234, Longman Scientific & Technical, Wiley, Essex, England, New York, 1990.; K. Rosenthal, Quantales and Their Applications, Pitman Research Notes in Mathematics Series, vol. 234, Longman Scientific & Technical, Wiley, Essex, England, New York, 1990. · Zbl 0703.06007
[21] Verwaat, W., Random upper semicontinuous functions and extremal processes, (Verwaat, W.; Holverda, H., Probability and Lattices (1997), CWI Tract, Centrum voor Wiskunde en Informatica), 1-56 · Zbl 0882.60003
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.