Michał Knapik's Home Page
I'm an assistant professor at ICS PAS. Earlier, I have been a postdoctoral researcher within Polish-Luxembourg VoteVerif project co-lead by Wojtek Jamroga. I defended a PhD thesis in Computer Science under supervision of Wojtek Penczek, also at ICS PAS.
So far, most my research was along the lines of specification and verification. I like both the theoretical and applied side of my work, and prefer to think of myself as an engineer with some math skills. I am always open to exciting opportunities from the industry and research community. It might sound cliché, but I do try to stay hungry, stay foolish, and love learning (albeit slowly) new things.
Contact: Michal.Knapik[LARCH]ipipan.waw.pl (put @ instead of the tree part!)
Selected Publications and Research
Most of the papers are downloadable PDFs. If you need a copy of something that is not available, please email me.
- 2019
- Wojciech Jamroga, Michał Knapik: Some Things are Easier for the Dumb and the Bright Ones (Beware the Average!), IJCAI 2019: 1734-1740
- Étienne André, Laure Petrucci, Wojciech Jamroga, Michał Knapik, Wojciech Penczek: Timed ATL: Forget Memory, Just Count, J. Artif. Intell. Res. 66: 197-223
- Wojciech Jamroga, Michał Knapik, Damian Kurpiewski and Łukasz Mikulski: Approximate Verification of Strategic Abilities under Imperfect Information, Artificial Intelligence
- Francesco Belardinelli, Rodica Condurache, Catalin Dima, Wojciech Jamroga, and Michał Knapik: Bisimulations for Verifying Strategic Abilities with an Application to the ThreeBallot Voting Protocol, Accepted for Information & Computation
- Damian Kurpiewski, Michał Knapik, and Wojciech Jamroga: On Domination and Control in Strategic Ability, AAMAS 2019
- Damian Kurpiewski, Michał Knapik, and Wojciech Jamroga: STV: Model Checking for Strategies under Imperfect Information (Demo), Demo Session at AAMAS 2019
- Laure Petrucci, Michal Knapik, Wojciech Penczek, Teofil Sidoruk: Squeezing State Spaces of (Attack-Defence) Trees, ICECCS 2019: 71-80
- 2018
- Wojciech Jamroga, Michał Knapik, Damian Kurpiewski: Model Checking the SELENE E-Voting Protocol in Multi-agent Logics, E-Vote-ID 2018: 100-116
- 2017
- Wojciech Jamroga, Michał Knapik, Damian Kurpiewski: Fixpoint Approximation of Strategic Abilities under Imperfect Information, AAMAS 2017: 1241-1249
- Étienne André, Laure Petrucci, Wojciech Jamroga, Michał Knapik, Wojciech Penczek: Timed ATL: Forget Memory, Just Count, AAMAS 2017: 1460-1462
- 2016
- Michał Knapik: Parametric Model Checking, PhD thesis
- Étienne André, Michał Knapik, Wojciech Penczek, Laure Petrucci: Controlling Actions and Time in Parametric Timed Automata, ACSD 2016: 45-54
- Michał Knapik, Wojciech Penczek: SMT-Based Parameter Synthesis for Parametric Timed Automata , Challenging Problems and Solutions in Intelligent Systems 2016: 3-21
- 2015
- Michał Knapik, Artur Męski, Wojciech Penczek: Action Synthesis for Branching Time Logic: Theory and Applications, ACM Trans. Embedded Comput. Syst. 14(4): 64:1-64:23
- Michał Knapik, Artur Niewiadomski, Wojciech Penczek: Generating None-Plans in Order to Find Plans, SEFM 2015: 310-324 (SEFM Best Paper Award)
- 2014
- Michał Knapik, Wojciech Penczek: Parameter Synthesis for Timed Kripke Structures , Fundam. Inform. 133(2-3): 211-226
- Michał Knapik, Artur Męski, Wojciech Penczek: Action Synthesis for Branching Time Logic: Theory and Applications, ACSD 2014: 1-10
- Michał Knapik, Wojciech Penczek: Fixed-Point Methods in Parametric Model Checking, IEEE Conf. on Intelligent Systems (1) 2014: 231-242
- 2013
- Michał Knapik, Wojciech Penczek: Parameter Synthesis for Timed Kripke Structures, CS&P 2013: 259-270
- 2012
- Andrew V. Jones, Michał Knapik, Wojciech Penczek, Alessio Lomuscio: Group synthesis for parametric temporal-epistemic logic, AAMAS 2012: 1107-1114 (Best Paper Award Nomination)
- Michał Knapik, Wojciech Penczek: SMT-based parameter synthesis for L/U automata, PNSE 2012: 77-92
- Michał Knapik, Wojciech Penczek: Bounded Model Checking for Parametric Timed Automata, Trans. Petri Nets and Other Models of Concurrency 5: 141-159
- 2010
- Michał Knapik, Wojciech Penczek, Maciej Szreter: Bounded Parametric Model Checking for Elementary Net Systems, Trans. Petri Nets and Other Models of Concurrency 4: 42-71
- Michał Knapik, Wojciech Penczek, Maciej Szreter, Agata Pólrola: Bounded Parametric Verification for Distributed Time Petri Nets with Discrete-Time Semantics, Fundam. Inform. 101(1-2): 9-27
- Michał Knapik, Artur Niewiadomski, Wojciech Penczek, Agata Pólrola, Maciej Szreter, Andrzej Zbrzezny: Parametric Model Checking with VerICS, Trans. Petri Nets and Other Models of Concurrency 4: 98-120
- Michał Knapik, Wojciech Penczek: Bounded Model Checking for Parametric Timed Automata, ACSD/Petri Nets Workshops 2010: 419-435
Theory of Distributed and Computing Systems Seminar
The seminar has been started by Wojtek Jamroga in 2015, I believe. The titles of the upcoming talks are always tentative and the talks are sometimes postponed or even canceled, so please send me an email if you wish to be informed in advance.
Upcoming talks
| Date | Title and Speaker |
|---|
Past (since March 2019)
| Date | Title and Speaker |
|---|---|
| 31.03.2022 | Rajeev Gore (Australian National University and ICS PAS), And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL, and CPDL. |
| 27.01.2022 | Rajeev Gore (Australian National University and ICS PAS), CEGAR-Tableaux: improved modal satisfiability via modal clause-learning and SAT |
| 18.11.2021 | Agnieszka Zbrzezny, On Guaranteed Optimal Robust Explanations for NLP Models |
| 14.10.2021 | Magdalena Kacprzak, Wojciech Penczek, Artur Niewiadomski, Satisfiability Checking for Strategy Logic |
| 16.09.2021 | Rajeev Gore (Vienna University of Technology and ICS PAS), Open Problem: Complex Voting Schemes. A Formally Verified Single Transferable Vote Scheme with Fractional Values |
| 8.07.2021 | Witold Pazderski (UMK & IPI PAN), Real-Time Exploration of Data |
| 17.06.2021 | Federica Adobbati (UNIMIB), Verification of properties on partially observable Petri nets |
| 10.06.2021 | Dilian Gurov (KTH), Knowledge-Based Strategies for Multi-Player Games with Imperfect Information |
| 20.05.2021 | Teofil Sidoruk (IPI PAN), About paper: 'Myrto Arapinis, Véronique Cortier, Steve Kremer: When Are Three Voters Enough for Privacy Properties?' |
| 29.04.2021 | Damian Kurpiewski (IPI PAN), w STV+Reductions |
| 25.03.2021 | Łukasz Maśko (IPI PAN), Distributed Model Checking of Multi-Agent Systems |
| 25.02.2021 | Teofil Sidoruk (IPI PAN), Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-Agent Systems |
| 18.02.2021 | Iwo Błądek and Krzysztof Krawiec (PUT), Counterexample-Driven Genetic Programming: Stochastic Synthesis of Provably Correct Programs |
| 28.I.2021 | Włodzimierz Drabent (ICS PAS), Answer Set Programming pt. 2 |
| 21.I.2021 | Włodzimierz Drabent (ICS PAS), Answer Set Programming pt. 1 |
| 3.12.2020 | Łukasz Mikulski (UMK and ICS PAS), Synthesis and Analysis of Concurrent Processes in Step Sequence Semantics, pt. 2 |
| 26.11.2020 | Łukasz Mikulski (UMK and ICS PAS), Synthesis and Analysis of Concurrent Processes in Step Sequence Semantics, pt. 1 |
| 22.10.2020 | Wojtek Jamroga (ICS PAS and University of Luxembourg), Pretty Good Strategies for Benaloh Challenge |
| 05.11.2020 | Damian Kurpiewski (ICS PAS), Natural Strategic Abilities in Voting Protocols |
| 1.10.2020 | Yan Kim (University of Luxembourg), Towards Model Checking of Voting Protocols in Uppaal |
| 16.07.2020 | Michał Knapik (ICS PAS), Towards Reductions for Live-Reset Trees |
| 02.07.2020 | Artur Niewiadomski (UPH Siedlce), Evolutionary, symbolic, and hybrid algorithms for planning and web-service composition |
| 4.06.2020 | Damian Kurpiewski (ICS PAS), Pretty Good Strategies and How to Find Them |
| 21.05.2020 | Teofil Sidoruk (ICS PAS), A Short Overview of Partial Order Reduction |
| 12.03.2020 | Wiktor B. Daszczuk (Politechnika Warszawska, Wydział Elektroniki i Technik Informacyjnych) 2 wagabundów: niewyczerpująca weryfikacja modelowa w służbie znajdowania częściowych zakleszczeń w olbrzymich systemach rozproszonych |
| 27.02.2020 | Tomasz Kuchta (Samsung R&D) Popular Testing Techniques and Tools Used in the Industry |
| 25.11.2019 | Łukasz Mikulski (UMK), Reversing Steps in Petri Nets |
| 7.11.2019 | Kamila Barylska (UMK), Reversible Computation vs. Reversibility in Petri Nets |
| 17.10.2019 | Wojtek Jamroga (IPI PAN and University of Luxembourg), Some Things are Easier for the Dumb and the Bright Ones (Beware the Average!) |
| 22.08.2019 | Laure Petrucci (Université Paris 13), Squeezing State Spaces of (Attack-Defence) Trees |
| 27.06.2019 | Michał Knapik (ICS PAS) On Domination and Control in Strategic Ability |
| 30.06.2019 | Beata Konikowska (ICS PAS) Temporal logic for exploration systems |
| 09.05.2019 | Laure Petrucci (Université Paris 13) Minimal-Time Synthesis for Parametric Timed Automata |
| 25.04.2019 | Eryk Laskowski (ICS PAS) Równoważenie obciążenia w środowisku JPPF (ang. Java Parallel Processing Framework) z wykorzystaniem optymalizacji ekstremalnej |
| 28.03.2019 | Benjamin Bordais (ENS Rennes) Ride sharing platform vs Taxi platform: the impact on the revenue |
| 21.03.2019 | Jörg Keller (FernUniversität Hagen) Static Scheduling for Parallel Computing - Challenges, Approaches, Applications |
| 14.03.2019 | Andrzej Mizera (Univ. of Luxembourg): Divide & Control: A Decomposition-based Approach towards the Control of Boolean Networks |