Top

Published in:

2020 | OriginalPaper | Chapter

Expressibility in the Kleene Algebra of Partial Predicates with the Complement Composition

Authors : Ievgen Ivanov, Mykola Nikitchenko

Published in: Information and Communication Technologies in Education, Research, and Industrial Applications

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

In the paper we investigate the expressibility of partial predicates in the Kleene algebra extended with the composition of predicate complement and give a necessary and sufficient condition of this expressibility in terms of the existence of an optimal solution of an optimization problem. We also investigate the expressibility in the first-order Kleene algebra with predicate complement. The obtained results may be useful for software verification using an extension of the Floyd-Hoare logic for partial pre- and postconditions.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter Optimized Term Extraction Method Based on Computing Merged Partial C-Values

next chapter Program-Oriented Logics of Renominative Level with Extended Renomination and Equality

The maximum cardinality of a subset such that any two of its distinct points are at the same distance.

If one interprets partiality in terms as possibility, minimization of ||f|| may be related to the principle of minimum specificity of D. Dubois et al. from possibility theory, or other similar principles.

Wiik, J., Boström, P.: Contract-based verification of MATLAB and simulink matrix-manipulating code. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 396–412. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11737-9_26CrossRef

Floyd, R.: Assigning meanings to programs. Math. Aspects Comput. Sci. 19, 19–32 (1967)MathSciNetCrossRef

Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRef

Ivanov, I., Korniłowicz, A., Nikitchenko, M.: Implementation of the composition-nominative approach to program formalization in Mizar. Comput. Sci. J. Moldova 26, 59–76 (2018)MathSciNetMATH

Ivanov, I., Korniłowicz, A., Nikitchenko, M.: Formalization of nominative data in Mizar. In: Proceedings of TAAPSD 2015, 23–26 December 2015, pp. 82–85. Taras Shevchenko National University of Kyiv, Ukraine (2015)

Ivanov, I.: An abstract block formalism for engineering systems. In: Ermolayev, V., et al. (eds.) Proceedings of the 9th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer, Kherson, Ukraine, June 19–22, 2013. CEUR Workshop Proceedings, vol. 1000, pp. 448–463. CEUR-WS.org (2013)

Ivanov, I.: On existence of total input-output pairs of abstract time systems. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds.) ICTERI 2013. CCIS, vol. 412, pp. 308–331. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03998-5_16CrossRef

Ivanov, I.: On representations of abstract systems with partial inputs and outputs. In: Gopal, T.V., Agrawal, M., Li, A., Cooper, S.B. (eds.) TAMC 2014. LNCS, vol. 8402, pp. 104–123. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06089-7_8CrossRef

Ivanov, I., Nikitchenko, M.: Inference rules for the partial floyd-hoare logic based on composition of predicate complement. In: Ermolayev, V., Suárez-Figueroa, M.C., Yakovyna, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A. (eds.) ICTERI 2018. CCIS, vol. 1007, pp. 71–88. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-13929-2_4CrossRef

10.

Korniłowicz, A., Ivanov, I., Nikitchenko, M.: Kleene algebra of partial predicates. Formalized Math. 26, 11–20 (2018)CrossRef

11.

Korniłowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: An approach to formalization of an extension of Floyd-Hoare logic. In: Proceedings of the 13th International Conference on ICT in Education, Research and Industrial Applications. Integration, Harmonization and Knowledge Transfer, Kyiv, Ukraine, May 15–18, 2017, pp. 504–523 (2017)

12.

Kornilowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: Formalization of the algebra of nominative data in Mizar. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2017 Federated Conference on Computer Science and Information Systems. ACSIS, vol. 11, pp. 237–244 (2017)

13.

Korniłowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: Formalization of the nominative algorithmic algebra in Mizar. In: Świątek, J., Borzemski, L., Wilimowska, Z. (eds.) ISAT 2017. AISC, vol. 656, pp. 176–186. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-67229-8_16CrossRef

14.

Kryvolap, A., Nikitchenko, M., Schreiner, W.: Extending floyd-hoare logic for partial pre- and postconditions. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds.) ICTERI 2013. CCIS, vol. 412, pp. 355–378. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03998-5_18CrossRef

15.

Nikitchenko, M., Kryvolap, A.: Properties of inference systems for Floyd-Hoare logic with partial predicates. Acta Electrotechnica et Informatica 13(4), 70–78 (2013)CrossRef

16.

Nikitchenko, M., Ivanov, I., Korniłowicz, A., Kryvolap, A.: Extended floyd-hoare logic over relational nominative data. In: Bassiliades, N., et al. (eds.) ICTERI 2017. CCIS, vol. 826, pp. 41–64. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-76168-8_3CrossRef

17.

Nikitchenko, N.S.: A composition nominative approach to program semantics. Technical report, IT-TR 1998–020, Technical University of Denmark (1998)

18.

Skobelev, V., Nikitchenko, M., Ivanov, I.: On algebraic properties of nominative data and functions. In: Ermolayev, V., Mayr, H., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds.) ICTERI 2014. CCIS, vol. 469, pp. 117–138. Springer, Cham (2014)CrossRef

19.

Yablonskii, S.: Functional constructions in a k-valued logic. Trudy Mat. Inst. Steklov. 51, 5–142 (1958)MathSciNet

20.

Nikitchenko, M., Shkilniak, O., Shkilniak, S., Mamedov, T.: Completeness of the logic of partial quasiary predicates with the complement composition. In: Proceedings of the Conference on Mathematical Foundations of Informatics MFOI 2019, July 3–6, 2019, Iasi, Romania (2019)

Title: Expressibility in the Kleene Algebra of Partial Predicates with the Complement Composition
Authors: Ievgen Ivanov
Mykola Nikitchenko
Publisher: Springer International Publishing
Book: Information and Communication Technologies in Education, Research, and Industrial Applications
Print ISBN: 978-3-030-39458-5

Electronic ISBN: 978-3-030-39459-2

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-39459-2_3

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner