Skip to main content
SpringerLink
Log in

On the Construction of Multi-valued Concurrent Dynamic Logics

  • Conference paper
  • First Online:
Dynamic Logic. New Trends and Applications (DALI 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12005))

Included in the following conference series:

  • 283 Accesses

Abstract

Dynamic logic is a powerful framework for reasoning about imperative programs. An extension with a concurrent operator, called concurrent propositional dynamic logic (CPDL) [20], was introduced to formalise programs running in parallel. In a different direction, other authors proposed a systematic method for generating multi-valued propositional dynamic logics to reason about weighted programs [15]. This paper presents the first step of combining these two frameworks to introduce uncertainty in concurrent computations. In the proposed framework, a weight is assigned to each branch of the parallel execution, resulting in a (possible) asymmetric parallelism, inherent to the fuzzy programming paradigm [2, 23]. By adopting such an approach, a family of logics is obtained, called multi-valued concurrent propositional dynamic logics (\(\mathcal {GCDL}(\mathbf {A})\)), parametric on an action lattice \(\mathbf {A}\) specifying a notion of “weight” assigned to program execution. Additionally, the validity of some axioms of CPDL is discussed in the new family of generated logics.

This work was founded by the ERDF—European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project POCI-01-0145-FEDER-030947.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Baltag, A., Smets, S.: The dynamic turn in quantum logic. Synthese 186(3), 753–773 (2012)

    Article  MathSciNet  Google Scholar 

  2. Cingolani, P., Alcalá-Fdez, J.: jFuzzylogic: a Java library to design fuzzy logic controllers according to the standard for fuzzy control programming. Int. J. Comput. Intell. Syst. 6(sup1), 61–75 (2013)

    Article  Google Scholar 

  3. Conway, J.: Regular Algebra and Finite Machines. Dover Publications, New York (1971)

    MATH  Google Scholar 

  4. den Hartog, J., de Vink, E.P.: Verifying probabilistic programs using a Hoare like logic. Int. J. Found. Comput. Sci. 13(3), 315–340 (2002)

    Article  MathSciNet  Google Scholar 

  5. den Hartog, J.I.: Probabilistic extensions of semantical models. Ph.D. thesis, Vrije Universiteit, Vrije (2002)

    Google Scholar 

  6. Furusawa, H., Kawahara, Y., Struth, G., Tsumagari, N.: Kleisli, Parikh and Peleg compositions and liftings for multirelations. J. Log. Algebraic Methods Program. 90, 84–101 (2017)

    Article  MathSciNet  Google Scholar 

  7. Furusawa, H., Struth, G.: Taming multirelations. ACM Trans. Comput. Log. 17(4), 28:1–28:34 (2016)

    Article  MathSciNet  Google Scholar 

  8. Gomes, L.: On the construction of multi-valued concurrent dynamic logic. CoRR abs/1911.00462 (2019)

    Google Scholar 

  9. Gomes, L., Madeira, A., Barbosa, L.S.: Generalising KAT to verify weighted computations. CoRR abs/1911.01146 (2019)

    Article  Google Scholar 

  10. Hoare, C.A.R.T., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 399–414. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04081-8_27

    Chapter  Google Scholar 

  11. Jipsen, P., Moshier, M.A.: Concurrent Kleene algebra with tests and branching automata. J. Log. Algebraic Method Program. 85(4), 637–652 (2016)

    Article  MathSciNet  Google Scholar 

  12. Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162–178 (1985)

    Article  MathSciNet  Google Scholar 

  13. Kozen, D.: On action algebras. In: Logic and the Flow of Information, Amsterdam (1993)

    Google Scholar 

  14. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110, 366–390 (1994)

    Article  MathSciNet  Google Scholar 

  15. Madeira, A., Neves, R., Martins, M.A.: An exercise on the generation of many-valued dynamic logics. JLAMP 1, 1–29 (2016)

    MATH  Google Scholar 

  16. Madeira, A., Neves, R., Martins, M.A., Barbosa, L.S.: A dynamic logic for every season. In: Braga, C., Martí-Oliet, N. (eds.) SBMF 2014. LNCS, vol. 8941, pp. 130–145. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15075-8_9

    Chapter  Google Scholar 

  17. Martin, C.E., Curtis, S.A., Rewitzky, I.: Modelling angelic and demonic nondeterminism with multirelations. Sci. Comput. Program. 65(2), 140–158 (2007)

    Article  MathSciNet  Google Scholar 

  18. McIver, A., Rabehaja, T., Struth, G.: An event structure model for probabilistic concurrent Kleene algebra. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 653–667. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_43

    Chapter  MATH  Google Scholar 

  19. Parikh, R.: Propositional game logic. In: 24th Annual Symposium on Foundations of Computer Science, pp. 195–200. IEEE Computer Society (1983)

    Google Scholar 

  20. Peleg, D.: Concurrent dynamic logic. J. ACM 34(2), 450–479 (1987)

    Article  MathSciNet  Google Scholar 

  21. Platzer, A.: Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14509-4

    Book  MATH  Google Scholar 

  22. Qiao, R., Wu, J., Wang, Y., Gao, X.: Operational semantics of probabilistic Kleene algebra with tests. In: Proceedings - IEEE Symposium on Computers and Communications, pp. 706–713 (2008)

    Google Scholar 

  23. Vetterlein, T., Mandl, H., Adlassnig, K.: Fuzzy arden syntax: a fuzzy programming language for medicine. Artif. Intell. Med. 49(1), 1–10 (2010)

    Article  Google Scholar 

  24. Zadeh, L.: Fuzzy sets. Inf. Control 8(3), 338–353 (1965)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. HASLab INESC TEC, Univ. Minho, Braga, Portugal

    Leandro Gomes

Authors
  1. Leandro Gomes
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Leandro Gomes .

Editor information

Editors and Affiliations

  1. University of Minho, Braga, Portugal

    Luís Soares Barbosa

  2. Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam, Noord-Holland, The Netherlands

    Alexandru Baltag

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Gomes, L. (2020). On the Construction of Multi-valued Concurrent Dynamic Logics. In: Soares Barbosa, L., Baltag, A. (eds) Dynamic Logic. New Trends and Applications. DALI 2019. Lecture Notes in Computer Science(), vol 12005. Springer, Cham. https://doi.org/10.1007/978-3-030-38808-9_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-38808-9_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-38807-2

  • Online ISBN: 978-3-030-38808-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation