Software and Computational Systems Lab

Publications of Martin Wirsing

1. Manfred Broy, Albrecht Schmidt, and Martin Wirsing. In memory of Heinrich Hussmann, long-time friend and SoSyM editor. Softw. Syst. Model., 22(2):453-454, 2023. doi:10.1007/s10270-023-01099-0 Publisher's Version PDF
   BibTeX Entry

   @article{NachrufHussmann, author = {Manfred Broy and Albrecht Schmidt and Martin Wirsing}, title = {In memory of Heinrich Hussmann, long-time friend and SoSyM editor}, journal = {Softw. Syst. Model.}, volume = {22}, number = {2}, pages = {453--454}, year = {2023}, doi = {10.1007/s10270-023-01099-0}, pdf = {https://sosy-lab.org/research/pub/2023-SoSyM.In_memory_of_Heinrich_Hussmann_long-time_friend_and_SoSyM_editor.pdf}, }
2. Martin Wirsing and and Alexander Knapp. A Reduction-based Cut-free Gentzen Calculus for Dynamic Epistemic Logic. Logic Journal of the IGPL, 12 2022. doi:10.1093/jigpal/jzac078 Publisher's Version PDF
   Abstract

   Dynamic epistemic logic (DEL) is a multi-modal logic for reasoning about the change of knowledge in multi-agent systems. It extends epistemic logic by a modal operator for actions which announce logical formulas to other agents. In Hilbert-style proof calculi for DEL, modal action formulas are reduced to epistemic logic, whereas current sequent calculi for DEL are labelled systems which internalize the semantic accessibility relation of the modal operators, as well as the accessibility relation underlying the semantics of the actions. We present a novel cut-free ordinary sequent calculus, called G4_P,A[], for propositional DEL. In contrast to the known sequent calculi, our calculus does not internalize the accessibility relations, but—similar to Hilbert style proof calculi—action formulas are reduced to epistemic formulas. Since no ordinary sequent calculus for full S5 modal logic is known, the proof rules for the knowledge operator and the Boolean operators are those of an underlying S4 modal calculus. We show the soundness and completeness of G4_P,A[] and prove also the admissibility of the cut-rule and of several other rules for introducing the action modality.
   BibTeX Entry

   @article{WirsingJ22, author = {Martin Wirsing and and Alexander Knapp}, title = {A Reduction-based Cut-free Gentzen Calculus for Dynamic Epistemic Logic}, journal = {Logic Journal of the IGPL}, year = {2022}, doi = {10.1093/jigpal/jzac078}, pdf = {https://sosy-lab.org/research/pub/2022-LogJIGPL.A_Reduction-based_Cut-free_Gentzen_Calculus_for_Dynamic_Epistemic_Logic.pdf}, abstract = {Dynamic epistemic logic (DEL) is a multi-modal logic for reasoning about the change of knowledge in multi-agent systems. It extends epistemic logic by a modal operator for actions which announce logical formulas to other agents. In Hilbert-style proof calculi for DEL, modal action formulas are reduced to epistemic logic, whereas current sequent calculi for DEL are labelled systems which internalize the semantic accessibility relation of the modal operators, as well as the accessibility relation underlying the semantics of the actions. We present a novel cut-free ordinary sequent calculus, called G4_P,A[], for propositional DEL. In contrast to the known sequent calculi, our calculus does not internalize the accessibility relations, but—similar to Hilbert style proof calculi—action formulas are reduced to epistemic formulas. Since no ordinary sequent calculus for full S5 modal logic is known, the proof rules for the knowledge operator and the Boolean operators are those of an underlying S4 modal calculus. We show the soundness and completeness of G4_P,A[] and prove also the admissibility of the cut-rule and of several other rules for introducing the action modality.}, issn = {1367-0751}, month = {12}, }
3. Martin Wirsing and Dieter Frey. Agile governance for innovating higher education teaching and learning. Rivista di Digital Politics(3/2021):543-558, 2021. Società editrice il Mulino. doi:10.53227/103804 Publisher's Version PDF
   BibTeX Entry

   @article{WirsingF21, author = {Martin Wirsing and Dieter Frey}, title = {Agile governance for innovating higher education teaching and learning}, journal = {Rivista di Digital Politics}, number = {3/2021}, pages = {543--558}, year = {2021}, publisher = {Società editrice il Mulino}, doi = {10.53227/103804}, pdf = {https://sosy-lab.org/research/pub/2022-Rivista.Agile_governance_for_innovating_higher_education_teaching_and_learning.pdf}, issn = {2785-0072}, urlpub = {https://www.rivisteweb.it/doi/10.53227/103804}, }
4. Lenz Belzner and Martin Wirsing. Synthesizing safe policies under probabilistic constraints with reinforcement learning and Bayesian model checking. Sci. Comput. Program., 206:102620, 2021. doi:10.1016/j.scico.2021.102620 Publisher's Version
   BibTeX Entry

   @article{DBLP:journals/scp/BelznerW21, author = {Lenz Belzner and Martin Wirsing}, title = {Synthesizing safe policies under probabilistic constraints with reinforcement learning and Bayesian model checking}, journal = {Sci. Comput. Program.}, volume = {206}, pages = {102620}, year = {2021}, doi = {10.1016/j.scico.2021.102620}, }
5. Simon Bliudze, Panagiotis Katsaros, Saddek Bensalem, and Martin Wirsing. On methods and tools for rigorous system design. Int. J. Softw. Tools Technol. Transf., 23(5):679-684, 2021. doi:10.1007/s10009-021-00632-0 Publisher's Version PDF
   BibTeX Entry

   @article{DBLP:journals/sttt/BliudzeKBW21, author = {Simon Bliudze and Panagiotis Katsaros and Saddek Bensalem and Martin Wirsing}, title = {On methods and tools for rigorous system design}, journal = {Int. J. Softw. Tools Technol. Transf.}, volume = {23}, number = {5}, pages = {679--684}, year = {2021}, doi = {10.1007/s10009-021-00632-0}, }
6. Rocco De Nicola, Stefan Jähnichen, and Martin Wirsing. Rigorous engineering of collective adaptive systems: special section. Int. J. Softw. Tools Technol. Transf., 22(4):389-397, 2020. doi:10.1007/s10009-020-00565-0 Publisher's Version PDF
   BibTeX Entry

   @article{DBLP:journals/sttt/NicolaJW20, author = {Rocco De Nicola and Stefan J{\"{a}}hnichen and Martin Wirsing}, title = {Rigorous engineering of collective adaptive systems: special section}, journal = {Int. J. Softw. Tools Technol. Transf.}, volume = {22}, number = {4}, pages = {389--397}, year = {2020}, doi = {10.1007/s10009-020-00565-0}, }
7. Dirk Beyer, Rolf Hennicker, Martin Hofmann, Tobias Nipkow, and Martin Wirsing. Software-Verifikation. In A. Bode, M. Broy, H.-J. Bungartz, and F. Matthes, editors, 50 Jahre Universitäts-Informatik in München, pages 75-86, 2017. Springer. doi:10.1007/978-3-662-54712-0_5 Keyword(s): Software Model Checking Publisher's Version PDF
   BibTeX Entry

   @incollection{InfMUC17, author = {Dirk Beyer and Rolf Hennicker and Martin Hofmann and Tobias Nipkow and Martin Wirsing}, title = {Software-Verifikation}, booktitle = {50 Jahre Universit{\"a}ts-Informatik in M{\"u}nchen}, editor = {A.~Bode and M.~Broy and H.-J.~Bungartz and F.~Matthes}, pages = {75-86}, year = {2017}, publisher = {Springer}, isbn = {978-3-662-54711-3}, doi = {10.1007/978-3-662-54712-0_5}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2017-50JahreInfMUC.Software-Verifikation.pdf}, keyword = {Software Model Checking}, }

8. Lenz Belzner, Thomas Gabor, and Martin Wirsing. Large Language Model Assisted Software Engineering: Prospects, Challenges, and a Case Study. In Bernhard Steffen, editors, Proc. AISoLA, LNCS 14380, 2023. Springer. To appear. PDF
   BibTeX Entry

   @inproceedings{WirsingAISoLA23, author = {Lenz Belzner and Thomas Gabor and Martin Wirsing}, title = {Large Language Model Assisted Software Engineering: Prospects, Challenges, and a Case Study}, booktitle = {Proc. AISoLA}, editor = {Bernhard Steffen}, year = {2023}, series = {LNCS~14380}, publisher = {Springer}, pdf = {https://sosy-lab.org/research/pub/2023-AISoLA.Large_Language_Model_Assisted_Software_Engineering.pdf}, note = {To appear.}, }
9. Martin Wirsing and Lenz Belzner. Towards Systematically Engineering Autonomous Systems using Reinforcement Learning and Planning. In In Pedro López-García, John P. Gallagher, and Roberto Giacobazzi, editors, Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems - Essays Dedicated to Manuel Hermenegildo on the Occasion of His 60th Birthday, LNCS 13160, pages 281-306, 2023. Springer. doi:10.1007/978-3-031-31476-6_16 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{WirsingAVERTIS23, author = {Martin Wirsing and Lenz Belzner}, title = {Towards Systematically Engineering Autonomous Systems using Reinforcement Learning and Planning}, booktitle = {Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems - Essays Dedicated to Manuel Hermenegildo on the Occasion of His 60th Birthday}, editor = {In Pedro López-García and John P. Gallagher and Roberto Giacobazzi}, pages = {281--306}, year = {2023}, series = {LNCS~13160}, publisher = {Springer}, doi = {10.1007/978-3-031-31476-6_16}, pdf = {https://sosy-lab.org/research/pub/2023-AVERTIS.Towards_Systematically_Engineering_Autonomous_Systems_using_Reinforcement_Learning_and_Planning.pdf}, }
10. Martin Wirsing, Rocco De Nicola, and Stefan Jähnichen. Rigorous Engineering of Collective Adaptive Systems Introduction to the 4th Track Edition. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part III, LNCS 13703, pages 3-12, 2022. Springer. doi:10.1007/978-3-031-19759-8_1 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{DBLP:conf/isola/WirsingNJ22, author = {Martin Wirsing and Rocco De Nicola and Stefan J{\"{a}}hnichen}, title = {Rigorous Engineering of Collective Adaptive Systems Introduction to the 4th Track Edition}, booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part {III}}, editor = {Tiziana Margaria and Bernhard Steffen}, pages = {3--12}, year = {2022}, series = {LNCS~13703}, publisher = {Springer}, doi = {10.1007/978-3-031-19759-8_1}, pdf = {https://sosy-lab.org/research/pub/2022-ISOLA.Rigorous_Engineering_of_Collective_Adaptive_Systems.pdf}, }
11. Rolf Hennicker, Alexander Knapp, and Martin Wirsing. Epistemic Ensembles. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part III, LNCS 13703, pages 110-126, 2022. Springer. doi:10.1007/978-3-031-19759-8_8 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{DBLP:conf/isola/HennickerKW22, author = {Rolf Hennicker and Alexander Knapp and Martin Wirsing}, title = {Epistemic Ensembles}, booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part {III}}, editor = {Tiziana Margaria and Bernhard Steffen}, pages = {110--126}, year = {2022}, series = {LNCS~13703}, publisher = {Springer}, doi = {10.1007/978-3-031-19759-8_8}, pdf = {https://sosy-lab.org/research/pub/2022-ISOLA.Epistemic_Ensembles.pdf}, }
12. Xiyue Sun, Fabian Pieroth, Kyrill Schmid, Martin Wirsing, and Lenz Belzner. On Learning Stable Cooperation in the Iterated Prisoner's Dilemma with Paid Incentives. In 42nd IEEE International Conference on Distributed Computing Systems, ICDCS Workshops, Bologna, Italy, July 10, 2022, pages 113-118, 2022. IEEE. doi:10.1109/ICDCSW56584.2022.00031 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{DBLP:conf/icdcs/SunPSWB22, author = {Xiyue Sun and Fabian Pieroth and Kyrill Schmid and Martin Wirsing and Lenz Belzner}, title = {On Learning Stable Cooperation in the Iterated Prisoner's Dilemma with Paid Incentives}, booktitle = {42nd {IEEE} International Conference on Distributed Computing Systems, {ICDCS} Workshops, Bologna, Italy, July 10, 2022}, pages = {113--118}, year = {2022}, publisher = {{IEEE}}, doi = {10.1109/ICDCSW56584.2022.00031}, pdf = {https://sosy-lab.org/research/pub/2022-ICDCSW.On_Learning_Stable_Cooperation_in_the_Iterated_Prisoners_Dilemma_with_Paid_Incentives.pdf}, }
13. Martin Wirsing, Rocco De Nicola, and Stefan Jähnichen. Rigorous Engineering of Collective Adaptive Systems Introduction to the 3rd Track Edition. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part II, LNCS 12477, pages 161-170, 2020. Springer. doi:10.1007/978-3-030-61470-6_10 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{DBLP:conf/isola/WirsingNJ20, author = {Martin Wirsing and Rocco De Nicola and Stefan J{\"{a}}hnichen}, title = {Rigorous Engineering of Collective Adaptive Systems Introduction to the 3rd Track Edition}, booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {II}}, editor = {Tiziana Margaria and Bernhard Steffen}, pages = {161--170}, year = {2020}, series = {LNCS~12477}, publisher = {Springer}, doi = {10.1007/978-3-030-61470-6\_10}, }
14. Rolf Hennicker and Martin Wirsing. A Dynamic Logic for Systems with Predicate-Based Communication. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part II, LNCS 12477, pages 224-242, 2020. Springer. doi:10.1007/978-3-030-61470-6_14 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{DBLP:conf/isola/HennickerW20, author = {Rolf Hennicker and Martin Wirsing}, title = {A Dynamic Logic for Systems with Predicate-Based Communication}, booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {II}}, editor = {Tiziana Margaria and Bernhard Steffen}, pages = {224--242}, year = {2020}, series = {LNCS~12477}, publisher = {Springer}, doi = {10.1007/978-3-030-61470-6\_14}, }