Projects funded by the NCN


Information on the principal investigator and host institution

Information of the project and the call

Keywords

Equipment

Delete all

Development and implementation of model checking methods for real-time and multi-agent systems

2011/01/B/ST6/05317

Keywords:

model checking multi-agent systems real-time systems temporal logics automata Petri nets

Descriptors:

  • ST6_3: Software engineering, operating systems, software development methods, programming languages

Panel:

ST6 - Computer science and informatics: informatics and information systems, computer science, scientific computing, intelligent systems

Host institution :

Akademia im. Jana Długosza w Częstochowie, Wydział Matematyczno-Przyrodniczy

woj. śląskie

Other projects carried out by the institution 

Principal investigator (from the host institution):

dr hab. Bożena Woźna-Szcześniak 

Number of co-investigators in the project: 3

Call: OPUS 1 - announced on 2011-03-15

Amount awarded: 272 500 PLN

Project start date (Y-m-d): 2011-12-08

Project end date (Y-m-d): 2014-12-07

Project duration:: 36 months (the same as in the proposal)

Project status: Project settled

Equipment purchased [PL]

  1. Monitor IIYAMA 23.6 CAL / E2480HSU-B1 LCD - OSPRZĘT STACJI SERWEROWEJ (1 000 PLN)
  2. Komputer DELL Vostro 470 I7-3770/32GB/SSD256/1TB/3YNBD - STACJA SERWEROWA (8 600 PLN)
  3. PRZEŁĄCZNIK EDIMAX KVM USB SOHO - OSPRZĘT STACJI SERWEROWEJ (200 PLN)
  4. MYSZ A4-TECH OPTYCZNA - OSPRZĘT STACJI SERWEROWEJ (150 PLN)
  5. Klawiatura Natec Slim USB - OSPRZĘT STACJI SERWEROWEJ (50 PLN)

Information in the final report

  • Publication in academic press/journals (7)
  • Articles in post-conference publications (16)
  • Book publications / chapters in book publications (3)
  1. BDD- versus SAT-based Bounded Model Checking for the Existential Fragment of Linear Temporal Logic with Knowledge: Algorithms and their Performance
    Authors:
    Artur Męski, Wojciech Penczek, Maciej Szreter, Bożena Woźna-Szcześniak, Andrzej Zbrzezny.
    Academic press:
    Journal of Autonomous Agents and Multi-Agent Systems (rok: 2014, tom: 28(4), strony: 558-604), Wydawca: Springer
    Status:
    Published
    DOI:
    10.1007/s10458-013-9232-2 - link to the publication
  2. Towards SAT-based BMC for LTLK over Interleaved Interpreted Systems
    Authors:
    Wojciech Penczek, Bożena Woźna-Szcześniak, Andrzej Zbrzezny
    Academic press:
    Fundamenta Informaticae (rok: 2012, tom: 119(3-4), strony: 373-392), Wydawca: IOS Press
    Status:
    Published
    DOI:
    10.3233/FI-2012-743 - link to the publication
  3. Verifying RTECTL properties of a train controller system
    Authors:
    Bożena Woźna-Szcześniak, Agnieszka Zbrzezny, Andrzej Zbrzezny
    Academic press:
    Prace Naukowe AJD w Częstochowie, Matematyka (rok: 2011, tom: XVI, strony: 153-162), Wydawca: Akademia im. Jana Długosza w Częstochowa
    Status:
    Published
  4. A translation of the existential model checking problem from MITL to HLTL
    Authors:
    Bożena Woźna-Szcześniak, Andrzej Zbrzezny
    Academic press:
    Fundamenta Informaticae (rok: 2013, tom: 122(4), strony: 401-420), Wydawca: IOS Press
    Status:
    Published
    DOI:
    10.3233/FI-2013-795 - link to the publication
  5. Checking EMTLK properties of Timed Interpreted Systems via Bounded Model Checking
    Authors:
    Bożena Woźna- Szcześniak, Andrzej Zbrzezny
    Academic press:
    Studia logica (rok: 2014, tom: -, strony: -), Wydawca: Springer
    Status:
    Submitted
  6. Checking MTL properties of Discrete Timed Automata via Bounded Model Checking.
    Authors:
    Bożena Woźna-Szcześniak, Andrzej Zbrzezny
    Academic press:
    Fundamenta Informaticae (rok: 2014, tom: 135(4), strony: 553-568), Wydawca: IOS Press
    Status:
    Published
    DOI:
    10.3233/FI-2014-1140 - link to the publication
  7. A new translation from ECTL* to SAT.
    Authors:
    Andrzej Zbrzezny
    Academic press:
    Fundamenta Informaticae (rok: 2012, tom: 120(3-4), strony: 375-395), Wydawca: IOS Press
    Status:
    Published
    DOI:
    10.3233/FI-2012-768 - link to the publication
  1. A Comparison of SAT-Based and SMT-Based Bounded Model Checking Methods for ECTL*
    Authors:
    Agnieszka Zbrzezny, Andrzej Zbrzezny
    Conference:
    The 23nd International Workshop on Concurrency, Specification and Programming (CS&P 2014) (rok: 2014, ), Wydawca: CEUR Workshop Proceedings (CEUR-WS.org), Sun SITE Central Europe
    Data:
    konferencja 29 Wrzesień - 1 Październik 2014
    Status:
    Published
  2. Bounded Model Checking for Linear Time Temporal-Epistemic Logic
    Authors:
    Artur Męski, Wojciech Penczek , Maciej Szreter
    Conference:
    Imperial College Computing Student Workshop (ICCSW'12) (rok: 2012, ), Wydawca: Schloss Dagstuhl
    Data:
    konferencja 27-28 wrzesień 2012, Londyn, Wielka Brytania
    Status:
    Published
  3. SAT-based Bounded Model Checking for Deontic Interleaved Interpreted Systems
    Authors:
    Bożena Woźna-Szcześniak, Andrzej Zbrzezny
    Conference:
    The 6th International KES Conference on Agents and Multi-agent Systems - Technologies and Applications (KES-AMSTA) (rok: 2012, ), Wydawca: Springer Berlin Heidelberg
    Data:
    konferencja 25-27 czerwiec 2012, Dubrownik, Chorwacja
    Status:
    Published
  4. SAT-based Bounded Model Checking for Weighted Deontic Interpreted Systems
    Authors:
    Bożena Woźna-Szcześniak
    Conference:
    The 16th Portuguese Conference on Artificial Intelligence (EPIA'2013) (rok: 2013, ), Wydawca: Springer
    Data:
    konferencja 9-12 wrzesień 2013
    Status:
    Published
  5. Bounded Model Checking for Knowledge and Linear Time
    Authors:
    Artur Męski, Wojciech Penczek, Maciej Szreter, Bożena Woźna-Szcześniak, Andrzej Zbrzezny
    Conference:
    The 11th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS'2012) (rok: 2012, ), Wydawca: IFAAMAS Press
    Data:
    konferencja 4-8 czerwiec 2012, Walencja, Hiszpania
    Status:
    Published
  6. Bounded Model Checking for Weighted Interpreted Systems and for Flat Weighted Epistemic Computation Tree Logic
    Authors:
    Bożena Woźna-Szcześniak, Ireneusz Szcześniak, Agnieszka Zbrzezny, Andrzej Zbrzezny
    Conference:
    The 17th International Conference on Principles and Practice of Multi-Agent Systems (PRIMA 2014) (rok: 2014, ), Wydawca: Springer-Verlag
    Data:
    konferencja 1-5 grudnia 2014, Gold Coast, Queensland, Australia
    Status:
    Published
  7. Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking (Extended Abstract)
    Authors:
    Bożena Woźna-Szcześniak, Andrzej Zbrzezny
    Conference:
    The 22nd International Workshop on Concurrency, Specification and Programming (CS&P 2013) (rok: 2013, ), Wydawca: CEUR Workshop Proceedings (CEUR-WS.org), Sun SITE Central Europe
    Data:
    konferencja 25-27 wrzesień 2013
    Status:
    Published
  8. Checking EMTLK properties of Timed Interpreted Systems via Bounded Model Checking (Short paper).
    Authors:
    Bożena Woźna-Szcześniak
    Conference:
    The 13th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS'2014) (rok: 2014, ), Wydawca: IFAAMAS Press
    Data:
    konferencja 5-9 Maj 2014
    Status:
    Published
  9. SAT-Based Bounded Model Checking for Weighted Interpreted Systems and Weighted Linear Temporal Logic
    Authors:
    Bożena Woźna-Szcześniak, Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Conference:
    The 16th International Conference on Principles and Practice of Multi-Agent Systems (PRIMA 2013) (rok: 2013, ), Wydawca: Springer
    Data:
    konferencja 1-6 grudzień 2013, Dunedin, Nowa Zelandia
    Status:
    Published
  10. Two Approaches to Bounded Model Checking for a Soft Real-Time Epistemic Computation Tree Logic
    Authors:
    Artur Męski, Bożena Woźna-Szcześniak, Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Conference:
    The 10th International Symposium on Distributed Computing and Artificial Intelligence (DCAI 2013) (rok: 2013, ), Wydawca: Springer
    Data:
    konferencja 22-24 maj 2013, Salamanka, Hiszpania
    Status:
    Published
  11. BDD-based Bounded Model Checking for LTLK over Two Variants of Interpreted Systems
    Authors:
    Artur Meski, Wojciech Penczek, Maciej Szreter
    Conference:
    The 5th International Workshop on Logics, Agents, and Mobility (LAM'12) (rok: 2012, ), Wydawca: CEUR Workshop Proceedings (CEUR-WS.org), Sun SITE Central Europe
    Data:
    konferencja 25-26 czerwiec 2012, Hamburg, Niemcy
    Status:
    Published
  12. SAT-based Bounded Model Checking for Weighted Deontic Interpreted Systems (Extended Abstract).
    Authors:
    Bożena Woźna-Szcześniak
    Conference:
    The 23nd International Workshop on Concurrency, Specification and Programming (CS&P 2014) (rok: 2014, ), Wydawca: CEUR Workshop Proceedings (CEUR-WS.org), Sun SITE Central Europe
    Data:
    konferencja 29 Wrzesień - 1 Październik 2014
    Status:
    Published
  13. On Boolean Encodings of Transition Relation for Parallel Compositions of Transition Systems
    Authors:
    Andrzej Zbrzezny
    Conference:
    The 22nd International Workshop on Concurrency, Specification and Programming (CS&P 2013) (rok: 2013, ), Wydawca: CEUR Workshop Proceedings (CEUR-WS.org), Sun SITE Central Europe
    Data:
    konferencja 25-27 wrzesień 2013
    Status:
    Published
  14. SAT-based BMC for Deontic Metric Temporal Logic and Deontic Interleaved Interpreted Systems.
    Authors:
    Bożena Woźna-Szcześniak, Andrzej Zbrzezny
    Conference:
    Declarative Agent Languages and Technologies X. The 10th International Workshop, (DALT 2012 ) (rok: 2013, ), Wydawca: Springer
    Data:
    konferencja 4 czerwiec 2012, Walencja, Hiszpania
    Status:
    Published
  15. SAT-based Bounded Model Checking for RTECTL and Simply-timed systems
    Authors:
    Bożena Woźna-Szcześniak, Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Conference:
    The 10th European Workshop on Performance Engineering (EPEW 2013) (rok: 2013, ), Wydawca: Springer
    Data:
    konferencja 16-17 wrzesień 2013
    Status:
    Published
  16. Two Approaches to Bounded Model Checking for Linear Time Logic with Knowledge
    Authors:
    Artur Męski, Wojciech Penczek, Maciej Szreter, Bożena Woźna-Szcześniak, Andrzej Zbrzezny
    Conference:
    The 6th International KES Conference on Agents and Multi-agent Systems - Technologies and Applications (KES-AMSTA) (rok: 2012, ), Wydawca: Springer Berlin Heidelberg
    Data:
    konferencja 25-27 czerwiec 2012, Dubrownik, Chorwacja
    Status:
    Published
  1. ROBDD-based Bounded Model Checking for DECTL and Simply-timed Systems
    Authors:
    Bożena Woźna-Szcześniak, Agnieszka Zbrzezny, Andrzej Zbrzezny
    Book:
    Selected Applications of Real Time Systems (rok: 2014, tom: Rozdział 5, strony: 51-62), Wydawca: Zeszyty Rady Naukowej Polskiego Towarzystwa Naukowego, oraz Wydawnictwo Nakom
    Status:
    Published
  2. SAT-based Bounded Model Checking for Metric Temporal Logic and Simply-timed systems
    Authors:
    Bożena Woźna-Szcześniak, Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Book:
    Designe, development and implementation of real time systems (rok: 2013, tom: Rozdział 14, strony: 181-190), Wydawca: Zeszyty Rady Naukowej Polskiego Towarzystwa Naukowego
    Status:
    Published
  3. On the SAT-based Verification of Communicative Commitments
    Authors:
    Bożena Woźna-Szcześniak.
    Book:
    Trends in Contemporary Computer Science (rok: 2014, tom: Rozdział 4, strony: 175-186), Wydawca: Politechnika Białostocka
    Status:
    Published