Kurpiewski, Damian; Jamroga, Wojciech; Maśko, Łukasz; Mikulski, Łukasz; Pazderski, Witold; Penczek, Wojciech; Sidoruk, Teofil Verification of multi-agent properties in electronic voting: a case study. (English) Zbl 07668114 Fernández-Duque, David (ed.) et al., Advances in modal logic. Vol. 14. Proceedings of the 14th conference (AiML 2022), Rennes, France, August 22–25, 2022. London: College Publications. 531-555 (2022). MSC: 68Q60 03B70 68T42 91A12 94A60 PDFBibTeX XMLCite \textit{D. Kurpiewski} et al., in: Advances in modal logic. Vol. 14. Proceedings of the 14th conference (AiML 2022), Rennes, France, August 22--25, 2022. London: College Publications. 531--555 (2022; Zbl 07668114) Full Text: arXiv
Jamroga, Wojciech; Konikowska, Beata; Kurpiewski, Damian; Penczek, Wojciech Multi-valued verification of strategic ability. (English) Zbl 1497.68307 Fundam. Inform. 175, No. 1-4, 207-251 (2020). MSC: 68Q60 03B44 68T42 PDFBibTeX XMLCite \textit{W. Jamroga} et al., Fundam. Inform. 175, No. 1--4, 207--251 (2020; Zbl 1497.68307) Full Text: DOI
André, Étienne; Knapik, Michał; Lime, Didier; Penczek, Wojciech; Petrucci, Laure Parametric verification: an introduction. (English) Zbl 1464.68224 Koutny, Maciej (ed.) et al., Transactions on Petri Nets and other Models of Concurrency XIV. Berlin: Springer. Lect. Notes Comput. Sci. 11790, 64-100 (2019). MSC: 68Q85 68Q60 PDFBibTeX XMLCite \textit{É. André} et al., Lect. Notes Comput. Sci. 11790, 64--100 (2019; Zbl 1464.68224) Full Text: DOI arXiv
Knapik, Michal Jozef; Andre, Etienne; Petrucci, Laure; Jamroga, Wojciech; Penczek, Wojciech Timed ATL: forget memory, just count. (English) Zbl 1430.68309 J. Artif. Intell. Res. (JAIR) 66, 197-223 (2019). MSC: 68T27 03B44 68Q60 PDFBibTeX XMLCite \textit{M. J. Knapik} et al., J. Artif. Intell. Res. (JAIR) 66, 197--223 (2019; Zbl 1430.68309) Full Text: DOI
Penczek, Wojciech (ed.); Schlingloff, Holger (ed.); Wasilewski, Piotr (ed.) Concurrency, specification, and programming: special issue of selected papers of CS&P 2017. Preface. (English) Zbl 1412.00049 Fundam. Inform. 165, No. 3-4, i-iii (2019). MSC: 00B25 68-06 68N30 68Q60 68Q85 PDFBibTeX XMLCite \textit{W. Penczek} (ed.) et al., Fundam. Inform. 165, No. 3--4, i-iii (2019; Zbl 1412.00049) Full Text: DOI
Alechina, Natasha (ed.); Nørvåg, Kjetil (ed.); Penczek, Wojciech (ed.) 25th international symposium on temporal representation and reasoning. TIME 2018, Warsaw, Poland, October 15–17, 2018. Proceedings. (English) Zbl 1402.68016 LIPIcs – Leibniz International Proceedings in Informatics 120. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-089-7). xiii, 23 articles, not consecutively paged, electronic only, open access (2018). MSC: 68-06 03B44 68Q60 68T27 00B25 PDFBibTeX XMLCite \textit{N. Alechina} (ed.) et al., 25th international symposium on temporal representation and reasoning. TIME 2018, Warsaw, Poland, October 15--17, 2018. Proceedings. Wadern: Schloss Dagstuhl -- Leibniz Zentrum für Informatik (2018; Zbl 1402.68016) Full Text: DOI Link
Czaja, Ludwik (ed.); Penczek, Wojciech (ed.); Schlingloff, Holger (ed.); Son, Nguyen Hung (ed.) Concurrency, specification, and programming: special issue of selected papers of CS&P 2016. Preface. (English) Zbl 1395.00064 Fundam. Inform. 157, No. 4, i-ii (2018). MSC: 00B25 68-06 68N30 68Q60 68Q85 PDFBibTeX XMLCite \textit{L. Czaja} (ed.) et al., Fundam. Inform. 157, No. 4, i-ii (2018; Zbl 1395.00064) Full Text: DOI
Męski, Artur; Koutny, Maciej; Penczek, Wojciech Verification of linear-time temporal properties for reaction systems with discrete concentrations. (English) Zbl 1378.68113 Fundam. Inform. 154, No. 1-4, 289-306 (2017). MSC: 68Q60 03B44 68Q05 PDFBibTeX XMLCite \textit{A. Męski} et al., Fundam. Inform. 154, No. 1--4, 289--306 (2017; Zbl 1378.68113) Full Text: DOI
Czaja, Ludwik (ed.); Penczek, Wojciech (ed.); Stencel, Krzysztof (ed.) Preface: Concurrency, specification and programming (CS&P). (English) Zbl 1360.00120 Fundam. Inform. 143, No. 1-2, v-vi (2016). MSC: 00B25 68-06 68Q60 68Q85 PDFBibTeX XMLCite \textit{L. Czaja} (ed.) et al., Fundam. Inform. 143, No. 1--2, v-vi (2016; Zbl 1360.00120) Full Text: DOI
Męski, Artur; Koutny, Maciej; Penczek, Wojciech Towards quantitative verification of reaction systems. (English) Zbl 1476.68092 Amos, Martyn (ed.) et al., Unconventional computation and natural computation. 15th international conference, UCNC 2016, Manchester, UK, July 11–15, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9726, 142-154 (2016). MSC: 68Q07 68Q60 PDFBibTeX XMLCite \textit{A. Męski} et al., Lect. Notes Comput. Sci. 9726, 142--154 (2016; Zbl 1476.68092) Full Text: DOI Link
Męski, Artur; Penczek, Wojciech; Rozenberg, Grzegorz Model checking temporal properties of reaction systems. (English) Zbl 1387.68167 Inf. Sci. 313, 22-42 (2015). MSC: 68Q60 68Q05 PDFBibTeX XMLCite \textit{A. Męski} et al., Inf. Sci. 313, 22--42 (2015; Zbl 1387.68167) Full Text: DOI
Knapik, Michał; Penczek, Wojciech Parameter synthesis for timed Kripke structures. (English) Zbl 1317.68118 Fundam. Inform. 133, No. 2-3, 211-226 (2014). MSC: 68Q60 68Q55 03B44 PDFBibTeX XMLCite \textit{M. Knapik} and \textit{W. Penczek}, Fundam. Inform. 133, No. 2--3, 211--226 (2014; Zbl 1317.68118) Full Text: DOI
Kurkowski, Miroslaw; Penczek, Wojciech Applying timed automata to model checking of security protocols. (English) Zbl 1304.68129 Wang, Jiacun (ed.), Handbook of finite state based models and applications. Boca Raton, FL: CRC Press (ISBN 978-1-4398-4618-6/hbk; 978-1-4398-4619-3/ebook). Discrete Mathematics and its Applications, 223-254 (2013). MSC: 68Q60 68M12 68Q45 94A60 PDFBibTeX XMLCite \textit{M. Kurkowski} and \textit{W. Penczek}, in: Handbook of finite state based models and applications. Boca Raton, FL: CRC Press. 223--254 (2013; Zbl 1304.68129)
Janowska, Agata; Penczek, Wojciech; Półrola, Agata; Zbrzezny, Andrzej Using integer time steps for checking branching time properties of time Petri nets. (English) Zbl 1395.68197 Koutny, Maciej (ed.) et al., Transactions on Petri Nets and Other Models of Concurrency VIII. Berlin: Springer (ISBN 978-3-642-40464-1/pbk). Lecture Notes in Computer Science 8100. Journal Subline, 89-105 (2013). MSC: 68Q85 68Q60 PDFBibTeX XMLCite \textit{A. Janowska} et al., Lect. Notes Comput. Sci. 8100, 89--105 (2013; Zbl 1395.68197) Full Text: DOI
Niewiadomski, Artur; Penczek, Wojciech; Półrola, Agata; Szreter, Maciej; Zbrzezny, Andrzej Towards automatic composition of web services: SAT-based concretisation of abstract scenarios. (English) Zbl 1254.68051 Fundam. Inform. 120, No. 2, 181-203 (2012). MSC: 68M11 68Q60 68R10 68T30 PDFBibTeX XMLCite \textit{A. Niewiadomski} et al., Fundam. Inform. 120, No. 2, 181--203 (2012; Zbl 1254.68051) Full Text: DOI
Jamroga, Wojciech; Penczek, Wojciech Specification and verification of multi-agent systems. (English) Zbl 1250.68190 Bezhanishvili, Nick (ed.) et al., Lectures on logic and computation. ESSLLI 2010 Copenhagen, Denmark, August 2010, ESSLLI 2011, Ljubljana, Slovenia, August 2011. Selected lecture notes. Berlin: Springer (ISBN 978-3-642-31484-1/pbk). Lecture Notes in Computer Science 7388, 210-263 (2012). MSC: 68Q60 03B45 68T27 68T42 91A99 91B14 PDFBibTeX XMLCite \textit{W. Jamroga} and \textit{W. Penczek}, Lect. Notes Comput. Sci. 7388, 210--263 (2012; Zbl 1250.68190) Full Text: DOI
Penczek, Wojciech; Woźna-Szcześniak, Bożena; Zbrzezny, Andrzej Towards SAT-based BMC for LTLK over interleaved interpreted systems. (English) Zbl 1279.68219 Fundam. Inform. 119, No. 3-4, 373-392 (2012). MSC: 68Q60 68T42 PDFBibTeX XMLCite \textit{W. Penczek} et al., Fundam. Inform. 119, No. 3--4, 373--392 (2012; Zbl 1279.68219) Full Text: DOI
Lomuscio, Alessio; Penczek, Wojciech Symbolic model checking for temporal-epistemic logic. (English) Zbl 1356.68144 Artikis, Alexander (ed.) et al., Logic programs, norms and action. Essays in honor of Marek J. Sergot on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-642-29413-6/pbk). Lecture Notes in Computer Science 7360. Lecture Notes in Artificial Intelligence, 172-195 (2012). MSC: 68Q60 03B42 03B44 PDFBibTeX XMLCite \textit{A. Lomuscio} and \textit{W. Penczek}, Lect. Notes Comput. Sci. 7360, 172--195 (2012; Zbl 1356.68144) Full Text: DOI
Knapik, Michał; Penczek, Wojciech Bounded model checking for parametric timed automata. (English) Zbl 1350.68183 Jensen, Kurt (ed.) et al., Transactions on Petri Nets and Other Models of Concurrency V. Berlin: Springer (ISBN 978-3-642-29071-8/pbk). Lecture Notes in Computer Science 6900. Journal Subline, 141-159 (2012). MSC: 68Q60 68Q45 68Q85 PDFBibTeX XMLCite \textit{M. Knapik} and \textit{W. Penczek}, Lect. Notes Comput. Sci. 6900, 141--159 (2012; Zbl 1350.68183) Full Text: DOI
Mȩski, Artur; Penczek, Wojciech; Półrola, Agata BDD-based bounded model checking for temporal properties of 1-safe Petri nets. (English) Zbl 1238.68086 Fundam. Inform. 109, No. 3, 305-321 (2011). Reviewer: Maciej Koutny (Newcastle upon Tyne) MSC: 68Q60 68Q85 68Q01 03B44 68N19 68M14 PDFBibTeX XMLCite \textit{A. Mȩski} et al., Fundam. Inform. 109, No. 3, 305--321 (2011; Zbl 1238.68086) Full Text: DOI
Lomuscio, Alessio; Penczek, Wojciech; Qu, Hongyang Partial order reductions for model checking temporal-epistemic logics over interleaved multi-agent systems. (English) Zbl 1213.68382 Fundam. Inform. 101, No. 1-2, 71-90 (2010). MSC: 68Q60 68T27 68T42 PDFBibTeX XMLCite \textit{A. Lomuscio} et al., Fundam. Inform. 101, No. 1--2, 71--90 (2010; Zbl 1213.68382) Full Text: DOI
Knapik, Michał; Penczek, Wojciech; Szreter, Maciej; Półrola, Agata Bounded parametric verification for distributed time Petri nets with discrete-time semantics. (English) Zbl 1213.68404 Fundam. Inform. 101, No. 1-2, 9-27 (2010). MSC: 68Q85 68Q60 PDFBibTeX XMLCite \textit{M. Knapik} et al., Fundam. Inform. 101, No. 1--2, 9--27 (2010; Zbl 1213.68404) Full Text: DOI
Knapik, Michał; Niewiadomski, Artur; Penczek, Wojciech; Półrola, Agata; Szreter, Maciej; Zbrzezny, Andrzej Parametric model checking with VerICS. (English) Zbl 1312.68134 Jensen, Kurt (ed.) et al., Transactions on Petri Nets and Other Models of Concurrency IV. Berlin: Springer (ISBN 978-3-642-18221-1/pbk). Lecture Notes in Computer Science 6550. Journal Subline, 98-120 (2010). MSC: 68Q60 68Q85 PDFBibTeX XMLCite \textit{M. Knapik} et al., Lect. Notes Comput. Sci. 6550, 98--120 (2010; Zbl 1312.68134) Full Text: DOI
Penczek, Wojciech; Pòłrola, Agata; Zbrzezny, Andrzej SAT-based (parametric) reachability for a class of distributed time Petri nets. (English) Zbl 1312.68137 Jensen, Kurt (ed.) et al., Transactions on Petri Nets and Other Models of Concurrency IV. Berlin: Springer (ISBN 978-3-642-18221-1/pbk). Lecture Notes in Computer Science 6550. Journal Subline, 72-97 (2010). MSC: 68Q60 68Q85 PDFBibTeX XMLCite \textit{W. Penczek} et al., Lect. Notes Comput. Sci. 6550, 72--97 (2010; Zbl 1312.68137) Full Text: DOI
Knapik, Michał; Szreter, Maciej; Penczek, Wojciech Bounded parametric model checking for elementary net systems. (English) Zbl 1312.68135 Jensen, Kurt (ed.) et al., Transactions on Petri Nets and Other Models of Concurrency IV. Berlin: Springer (ISBN 978-3-642-18221-1/pbk). Lecture Notes in Computer Science 6550. Journal Subline, 42-71 (2010). MSC: 68Q60 68Q85 PDFBibTeX XMLCite \textit{M. Knapik} et al., Lect. Notes Comput. Sci. 6550, 42--71 (2010; Zbl 1312.68135) Full Text: DOI
Penczek, Wojciech (ed.) Special issue: Concurrency specification and programming (CS&P). Selected papers based on the presentations at the workshop, Kraków-Przegorzały, Poland, September 28–30, 2009. (English) Zbl 1217.68016 Fundam. Inform. 102, No. 1, v, 113 p. (2010). MSC: 68-06 68Q60 68Q85 00B25 PDFBibTeX XML
Niewiadomski, Artur; Penczek, Wojciech; Szreter, Maciej Towards checking parametric reachability for UML state machines. (English) Zbl 1274.68199 Pnueli, Amir (ed.) et al., Perspectives of systems informatics. 7th international Andrei Ershov memorial conference, PSI 2009, Novosibirsk, Russia, June 15–19, 2009. Revised papers. Berlin: Springer (ISBN 978-3-642-11485-4/pbk). Lecture Notes in Computer Science 5947, 319-330 (2010). MSC: 68Q60 PDFBibTeX XMLCite \textit{A. Niewiadomski} et al., Lect. Notes Comput. Sci. 5947, 319--330 (2010; Zbl 1274.68199) Full Text: DOI
Niewiadomski, Artur; Penczek, Wojciech; Szreter, Maciej A new approach to model checking of UML state machines. (English) Zbl 1189.68077 Fundam. Inform. 93, No. 1-3, 289-303 (2009). MSC: 68Q60 PDFBibTeX XMLCite \textit{A. Niewiadomski} et al., Fundam. Inform. 93, No. 1--3, 289--303 (2009; Zbl 1189.68077)
Kurkowski, Mirosław; Penczek, Wojciech Timed automata based model checking of timed security protocols. (English) Zbl 1189.68075 Fundam. Inform. 93, No. 1-3, 245-259 (2009). MSC: 68Q60 68P25 68Q45 94A62 PDFBibTeX XMLCite \textit{M. Kurkowski} and \textit{W. Penczek}, Fundam. Inform. 93, No. 1--3, 245--259 (2009; Zbl 1189.68075)
Lomuscio, Alessio; Penczek, Wojciech; Qu, Hongyang Towards partial order reduction for model checking temporal epistemic logic. (English) Zbl 1226.68043 Peled, Doron A. (ed.) et al., Model checking and artificial intelligence. 5th international workshop, MoChArt 2008, Patras, Greece, July 21, 2008. Revised selected and invited papers. Berlin: Springer (ISBN 978-3-642-00430-8/pbk). Lecture Notes in Computer Science 5348. Lecture Notes in Artificial Intelligence, 106-121 (2009). MSC: 68Q60 03B42 03B44 68T27 68T42 PDFBibTeX XMLCite \textit{A. Lomuscio} et al., Lect. Notes Comput. Sci. 5348, 106--121 (2009; Zbl 1226.68043) Full Text: DOI
Penczek, Wojciech; Szreter, Maciej SAT-based unbounded model checking of timed automata. (English) Zbl 1159.68480 Fundam. Inform. 85, No. 1-4, 425-440 (2008). MSC: 68Q60 68Q45 PDFBibTeX XMLCite \textit{W. Penczek} and \textit{M. Szreter}, Fundam. Inform. 85, No. 1--4, 425--440 (2008; Zbl 1159.68480)
Lomuscio, Alessio; Penczek, Wojciech LDYIS: a framework for model checking security protocols. (English) Zbl 1160.68443 Fundam. Inform. 85, No. 1-4, 359-375 (2008). MSC: 68Q60 94A60 PDFBibTeX XMLCite \textit{A. Lomuscio} and \textit{W. Penczek}, Fundam. Inform. 85, No. 1--4, 359--375 (2008; Zbl 1160.68443)
Kacprzak, Magdalena; Nabiałek, Wojciech; Niewiadomski, Artur; Penczek, Wojciech; Półrola, Agata; Szreter, Maciej; Woźna, Bożena; Zbrzezny, Andrzej VERICS 2007 – a model checker for knowledgee and real-time. (English) Zbl 1167.68381 Fundam. Inform. 85, No. 1-4, 313-328 (2008). MSC: 68Q60 PDFBibTeX XMLCite \textit{M. Kacprzak} et al., Fundam. Inform. 85, No. 1--4, 313--328 (2008; Zbl 1167.68381)
Lomuscio, Alessio; Penczek, Wojciech; Woźna, Bożena Bounded model checking for knowledge and real time. (English) Zbl 1168.68422 Artif. Intell. 171, No. 16-17, 1011-1038 (2007). MSC: 68Q60 68T27 PDFBibTeX XMLCite \textit{A. Lomuscio} et al., Artif. Intell. 171, No. 16--17, 1011--1038 (2007; Zbl 1168.68422) Full Text: DOI
Kurkowski, Mirosław; Penczek, Wojciech; Zbrzezny, Andrzej SAT-based verification of security protocols via translation to networks of automata. (English) Zbl 1196.68140 Edelkamp, Stefan (ed.) et al., Model checking and artificial intelligence. 4th workshop, MoChArt IV, Riva del Garda, Italy, August 29, 2006. Revised selected and invited papers. Berlin: Springer (ISBN 978-3-540-74127-5/pbk). Lecture Notes in Computer Science 4428. Lecture Notes in Artificial Intelligence, 146-165 (2007). MSC: 68Q60 68M12 94A62 PDFBibTeX XMLCite \textit{M. Kurkowski} et al., Lect. Notes Comput. Sci. 4428, 146--165 (2007; Zbl 1196.68140) Full Text: DOI
Janowska, Agata; Penczek, Wojciech Path compression in timed automata. (English) Zbl 1124.68054 Fundam. Inform. 79, No. 3-4, 379-399 (2007). MSC: 68Q45 68Q60 PDFBibTeX XMLCite \textit{A. Janowska} and \textit{W. Penczek}, Fundam. Inform. 79, No. 3--4, 379--399 (2007; Zbl 1124.68054)
Kacprzak, Magdalena; Lomuscio, Alessio; Niewiadomski, Artur; Penczek, Wojciech; Raimondi, Franco; Szreter, Maciej Comparing BDD and SAT based techniques for model checking Chaum’s dining cryptographers protocol. (English) Zbl 1097.68074 Fundam. Inform. 72, No. 1-3, 215-234 (2006). MSC: 68Q60 PDFBibTeX XMLCite \textit{M. Kacprzak} et al., Fundam. Inform. 72, No. 1--3, 215--234 (2006; Zbl 1097.68074)
Penczek, Wojciech; Półrola, Agata Advances in verification of time Petri nets and timed automata. A temporal logic approach. (English) Zbl 1110.68087 Studies in Computational Intelligence 20. Berlin: Springer (ISBN 3-540-32869-6/hbk). xxxii, 257 p. (2006). Reviewer: Ryszard Janicki (Hamilton) MSC: 68Q85 68Q45 68Q60 03B44 68N30 68-02 PDFBibTeX XMLCite \textit{W. Penczek} and \textit{A. Półrola}, Advances in verification of time Petri nets and timed automata. A temporal logic approach. Berlin: Springer (2006; Zbl 1110.68087) Full Text: DOI
Woźna, Bożena; Lomuscio, Alessio; Penczek, Wojciech Bounded model checking for deontic interpreted systems. (English) Zbl 1272.68279 van der Hoek, Wiebe (ed.) et al., Proceedings of the 2nd international workshop on logic and communication in multi-agent systems, LCMAS, Nancy, France, August, 16–20, 2004. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 126, 93-114 (2005). MSC: 68Q60 68T27 68T42 PDFBibTeX XMLCite \textit{B. Woźna} et al., Electron. Notes Theor. Comput. Sci. 126, 93--114 (2005; Zbl 1272.68279) Full Text: Link
Półrola, Agata; Penczek, Wojciech; Szreter, Maciej Towards efficient partition refinement for checking reachability in timed automata. (English) Zbl 1099.68649 Larsen, Kim G. (ed.) et al., Formal modeling and analysis of timed systems. First international workshop, FORMATS 2003, Marseille, France, September 6–7, 2003. Revised papers. Berlin: Springer (ISBN 3-540-21671-5/pbk). Lecture Notes in Computer Science 2791, 2-17 (2004). MSC: 68Q45 68Q60 68Q85 PDFBibTeX XMLCite \textit{A. Półrola} et al., Lect. Notes Comput. Sci. 2791, 2--17 (2004; Zbl 1099.68649) Full Text: DOI
Penczek, Wojciech; Półrola, Agata Specification and model checking of temporal properties in time Petri nets and timed automata. (English) Zbl 1094.68067 Cortadella, Jordi (ed.) et al., Applications and theory of Petri nets 2004. 25th international conference, ICATPN 2004, Bologna, Italy, June 21–25, 2004. Proceedings. Berlin: Springer (ISBN 3-540-22236-7/pbk). Lecture Notes in Computer Science 3099, 37-76 (2004). MSC: 68Q85 68Q60 PDFBibTeX XMLCite \textit{W. Penczek} and \textit{A. Półrola}, Lect. Notes Comput. Sci. 3099, 37--76 (2004; Zbl 1094.68067) Full Text: DOI
Kacprzak, M.; Penczek, W. A SAT-based approach to unbounded model checking for alternating-time temporal epistemic logic. (English) Zbl 1072.03012 Synthese 142, No. 2, 203-227 (2004). MSC: 03B42 03B44 68T27 03B35 68Q60 PDFBibTeX XMLCite \textit{M. Kacprzak} and \textit{W. Penczek}, Synthese 142, No. 2, 203--227 (2004; Zbl 1072.03012) Full Text: DOI
Konikowska, Beata; Penczek, Wojciech On designated values in multi-valued \(\text{CTL}^*\) model checking. (English) Zbl 1083.68071 Fundam. Inform. 60, No. 1-4, 211-224 (2004). MSC: 68Q60 PDFBibTeX XMLCite \textit{B. Konikowska} and \textit{W. Penczek}, Fundam. Inform. 60, No. 1--4, 211--224 (2004; Zbl 1083.68071) Full Text: Link
Woźna, Bożena; Zbrzezny, Andrzej; Penczek, Wojciech Checking reachability properties for timed automata via SAT. (English) Zbl 1111.68548 Fundam. Inform. 55, No. 2, 223-241 (2003). MSC: 68Q85 68Q45 68Q60 PDFBibTeX XMLCite \textit{B. Woźna} et al., Fundam. Inform. 55, No. 2, 223--241 (2003; Zbl 1111.68548)
Penczek, Wojciech; Lomuscio, Alessio Verifying epistemic properties of multi-agent systems via bounded model checking. (English) Zbl 1111.68512 Fundam. Inform. 55, No. 2, 167-185 (2003). MSC: 68Q60 68Q85 68T05 PDFBibTeX XMLCite \textit{W. Penczek} and \textit{A. Lomuscio}, Fundam. Inform. 55, No. 2, 167--185 (2003; Zbl 1111.68512)
Konikowska, Beata; Penczek, Wojciech Model checking for multi-valued computation tree logics. (English) Zbl 1049.03026 Fitting, Melvin (ed.) et al., Beyond two: Theory and applications of multiple-valued logic. Heidelberg: Physica-Verlag (ISBN 3-7908-1541-1/pbk). Stud. Fuzziness Soft Comput. 114, 193-210 (2003). Reviewer: Damas Gruska (Bratislava) MSC: 03B70 68Q60 PDFBibTeX XMLCite \textit{B. Konikowska} and \textit{W. Penczek}, Stud. Fuzziness Soft Comput. 114, 193--210 (2003; Zbl 1049.03026)
Dembiński, Piotr; Janowska, Agata; Janowski, Paweł; Penczek, Wojciech; Półrola, Agata; Szreter, Maciej; Wozna, Bozena; Zbrzezny, Andrzej \(\surd\)erics: A tool for verifying timed automata and Estelle specifications. (English) Zbl 1031.68546 Garavel, Hubert (ed.) et al., Tools and algorithms for the construction and analysis of systems. 9th international conference TACAS 2003, held as part of the joint European conferences on theory and practice of software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2619, 278-283 (2003). MSC: 68Q60 PDFBibTeX XMLCite \textit{P. Dembiński} et al., Lect. Notes Comput. Sci. 2619, 278--283 (2003; Zbl 1031.68546) Full Text: Link
Penczek, Wojciech; Woźna, Boẓena; Zbrzezny, Andrzej Towards bounded model checking for the universal fragment of TCTL. (English) Zbl 1278.68192 Damm, Werner (ed.) et al., Formal techniques in real-time and fault-tolerant systems. 7th international symposium, FTRTFT 2002, co-sponsored by IFIP WG 2.2, Oldenburg, Germany, September 9–12, 2002. Proceedings. Berlin: Springer (ISBN 3-540-44165-4/pbk). Lecture Notes in Computer Science 2469, 265-288 (2002). MSC: 68Q60 68Q45 PDFBibTeX XMLCite \textit{W. Penczek} et al., Lect. Notes Comput. Sci. 2469, 265--288 (2002; Zbl 1278.68192) Full Text: DOI
Penczek, Wojciech Efficient model checking of causal-knowledge protocols. (English) Zbl 1053.68698 Dunin-Kȩplicz, Barbara (ed.) et al., From theory to practice in multi-agent systems. 2nd international workshop of central and eastern Europe, CEEMAS 2001 Cracow, Poland, September 26-29, 2001. Revised Papers. Berlin: Springer (ISBN 3-540-43370-8). Lect. Notes Comput. Sci. 2296, 242-252 (2002). MSC: 68T30 68Q60 PDFBibTeX XMLCite \textit{W. Penczek}, Lect. Notes Comput. Sci. 2296, 242--252 (2002; Zbl 1053.68698) Full Text: Link
Konikowska, Beata; Penczek, Wojciech Reducing model checking from multi-valued \(\text{CTL}^{\ast}\) to \(\text{CTL}^{\ast}\). (English) Zbl 1012.68132 Brim, Luboš (ed.) et al., CONCUR 2002 - concurrency theory. 13th international conference, Brno, Czech Republic, August 20-23, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2421, 226-239 (2002). MSC: 68Q85 68Q60 03B70 03B44 PDFBibTeX XMLCite \textit{B. Konikowska} and \textit{W. Penczek}, Lect. Notes Comput. Sci. 2421, 226--239 (2002; Zbl 1012.68132) Full Text: Link
Penczek, Wojciech; Woźna, Bożena; Zbrzezny, Andrzej Bounded model checking for the universal fragment of CTL. (English) Zbl 1052.68087 Fundam. Inform. 51, No. 1-2, 135-156 (2002). MSC: 68Q60 68Q85 03B44 PDFBibTeX XMLCite \textit{W. Penczek} et al., Fundam. Inform. 51, No. 1--2, 135--156 (2002; Zbl 1052.68087)
Ambroszkiewicz, Stanislaw; Penczek, Wojciech; Nowak, Tomasz Towards formal specification and verification in cyberspace. (English) Zbl 0988.68564 Rash, James L. (ed.) et al., Formal approaches to agent-based systems. 1st international workshop, FAABS 2000, Greenbelt, MD, USA, April 5-7, 2000. Revised papers. Berlin: Springer. Lect. Notes Comput. Sci. 1871, 16-32 (2001). MSC: 68Q60 68N19 68T99 68M14 68Q85 PDFBibTeX XMLCite \textit{S. Ambroszkiewicz} et al., Lect. Notes Comput. Sci. 1871, 16--32 (2001; Zbl 0988.68564)
Penczek, Wojciech; Półrola, Agata Abstractions and partial order reductions for checking branching properties of time Petri nets. (English) Zbl 0986.68096 Colom, José-Manuel (ed.) et al., Applications and theory of Petri nets 2001. 22nd international conference, ICATPN 2001, Newcastle upon Tyne, GB, June 25-29, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2075, 323-342 (2001). MSC: 68Q85 68Q60 PDFBibTeX XMLCite \textit{W. Penczek} and \textit{A. Półrola}, Lect. Notes Comput. Sci. 2075, 323--342 (2001; Zbl 0986.68096) Full Text: Link
Penczek, Wojciech; Szreter, Maciej; Gerth, Rob; Kuiper, Ruurd Improving partial order reductions for universal branching time properties. (English) Zbl 0966.68126 Fundam. Inform. 43, No. 1-4, 245-267 (2000). MSC: 68Q60 68N19 PDFBibTeX XMLCite \textit{W. Penczek} et al., Fundam. Inform. 43, No. 1--4, 245--267 (2000; Zbl 0966.68126)
Gerth, Rob; Kuiper, Ruurd; Peled, Doron; Penczek, Wojciech A partial order approach to branching time logic model checking. (English) Zbl 1045.68588 Inf. Comput. 150, No. 2, 132-152 (1999). MSC: 68Q60 03B44 03B70 68Q85 PDFBibTeX XMLCite \textit{R. Gerth} et al., Inf. Comput. 150, No. 2, 132--152 (1999; Zbl 1045.68588) Full Text: DOI Link
Penczek, Wojciech; Srebrny, Marian A complete axiomatization of a first-order temporal logic over trace systems. (English) Zbl 0883.68089 Peled, Doron A. (ed.) et al., Partial order methods in verification. DIMACS workshop, July 24-26, 1996, Princeton Univ., Princeton, NJ, USA. Providence, RI: AMS, American Mathematical Society. DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 29, 79-97 (1997). MSC: 68Q60 03B45 03B48 03B70 PDFBibTeX XMLCite \textit{W. Penczek} and \textit{M. Srebrny}, DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 29, 79--97 (1997; Zbl 0883.68089)
Kwiatkowska, M.; Peled, D.; Penczek, W. A hierarchy of partial order temporal properties. (English) Zbl 0949.68537 Gabbay, Dov M. (ed.) et al., Temporal logic. 1st International Conference, ICTL ’94, Bonn, Germany, July 11-14, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 827, 398-414 (1994). MSC: 68Q60 68Q55 03B44 68Q45 54H05 PDFBibTeX XMLCite \textit{M. Kwiatkowska} et al., Lect. Notes Comput. Sci. 827, 398--414 (1994; Zbl 0949.68537)
Penczek, Wojciech Temporal logics for trace systems: On automated verification. (English) Zbl 0783.68081 Int. J. Found. Comput. Sci. 4, No. 1, 31-67 (1993). MSC: 68Q60 68Q10 PDFBibTeX XMLCite \textit{W. Penczek}, Int. J. Found. Comput. Sci. 4, No. 1, 31--67 (1993; Zbl 0783.68081) Full Text: DOI
Penczek, Wojciech A temporal logic for event structures. (English) Zbl 0789.03030 Mathematical logic, Proc. Summer Sch. Conf. Ded. 90th Anniv. Arend Heyting, Chaika/Bulg. 1988, 327-338 (1990). Reviewer: J.-J.Ch.Meyer (Utrecht) MSC: 03B70 03B45 68Q60 PDFBibTeX XMLCite \textit{W. Penczek}, in: Mathematical logic. Proceedings of the summer school and conference dedicated to the ninetieth anniversary of Arend Heyting (1898-1980), held in Chaika, Bulgaria, September 13-23, 1988. New York: Plenum Press. 327--338 (1990; Zbl 0789.03030)