About the project
Propositional Dynamic Logic, PDL, is a well-known logic analysing discourse about action, in particular about effects of structured actions. Being based on classical logic, it is not adequate for analysing discourse where actions and their effects are specified using graded, vague or imprecise concepts. This project will develop graded, or many-valued, versions of PDL and its fragments (such as Kleene algebra) that are more suitable for this task. Hence, the project will contribute to the study of formal methods applicable in areas such as theory of action and applied ethics.
In particular, we will develop and study versions of weighted PDL and Kleene algebra based on Łukasiewicz, Gödel and product fuzzy logic and we will establish their basic mathematical properties. We will study applications of these logics in formalizing reasoning about collective agency and deontic aspects of action in situations involving graded notions, and for analysing reasoning about probabilistic aspects of action. We will also consider applications of these logics in formalizing reasoning about probabilistic programs.
The project is based at the Institute of Computer Science of the Czech Academy of Sciences and funded by the Czech Science Foundation, grant no. 22-16111S. It runs from January 2022 till December 2024.
Project team
Chun-Yu Lin
Igor Sedlár (PI)
Results
Weighted Kleene algebra with tests. We initiated the study of a weighted version of Kleene algebra with tests and we applied it to the study of weighted programs [C1], in particular to reasoning about weighted weakest preconditions for weighted programs [C2]. We established completeness results for finitely weighted Kleene algebras with tests with respect to models based on weighted sets of guarded strings and weighted binary relations [C3].
Workshops
- Prague Workshop on Kleene Algebra and Many-Valued Logic (28–29 November 2023)
Publications
Papers in conference proceedings:
-
[C1] I. Sedlár: Kleene Algebra With Tests for Weighted Programs. In: 53rd IEEE International Symposium on Multiple-Valued Logic (ISMVL 2023), pp. 111-116. IEEE, 2023.
- [C2] I. Sedlár: Kleene Algebra of Weighted Programs With Domain. In: Dynamic Logic. New Trends and Applications (DaLí 2023), pp. 52-67. Springer, 2023.
- [C3] I. Sedlár: Completeness of Finitely Weighted Kleene Algebra with Tests. In: Logic, Language, Information, and Computation (WoLLIC 2024), pp. 210-224. Springer, 2024.
Conference presentations
- I. Sedlár: Finitely Weighted Kleene Algebras With Tests. TACL 2024. Barcelona, Spain, 1-5 July 2024.
- O. Majer: A Logic of Probability Dynamics. CLoCK + Trends in Logic 2024. Krakow, Poland, 18-21 June 2024.
- I. Sedlár: Completeness of Finitely Weighted Kleene Algebra With Tests. WoLLIC 2024. Bern, Switzerland, 10-13 June 2024.
- O. Majer: A Logic of Probability Dynamics. Czech Gathering of Logicians 2024. Brno, Czech Republic, 27-28 May 2024.
- Ch. Lin: Concurrent Finitely-valued Dynamic Logic for Reasoning About Group Agency. MOSAIC 2023. Vienna, Austria, 27-29 September, 2023.
- O. Majer, I. Sedlár: Weighted Programs and Ethical Planning TbiLLC 2023. Telavi, Georgia, 18-22 September 2023.
- I. Sedlár: Kleene Algebras for Weighted Programs (invited talk). DaLí 2023. Tbilisi, Georgia, 15-16 September 2023.
- I. Sedlár: Kleene Algebra of Weighted Programs With Domain. DaLí 2023. Tbilisi, Georgia, 15-16 September 2023.
- I. Sedlár: Adding Weights to Kleene Algebra. Czech Gathering of Logicians 2023. Ostrava, Czech Republic, 1-2 June, 2023.
- I. Sedlár: Kleene Algebra With Tests for Weighted Programs. ISMVL 2023. Matsue, Japan, 22-24 May 2023.