SAT-based Bounded Model Checking for Weighted Deontic Interpreted Systems

Issue title: Concurrency, Specification and Programming (CS&P)

Guest editors: Ludwik Czaja, Wojciech Penczek and Krzysztof Stencel

Article type: Research Article

Authors: Woźna-Szcześniak, Bożena^*

Affiliations: IM&CS, Jan Długosz University in Częstochowa, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland. [email protected]

Correspondence: [*] Address for correspondence: IM&CS, Jan Długosz University in Częstochowa, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Abstract: We present WECTL*KD, a weighted branching time temporal logic to specify knowledge, and correct functioning behaviour in multi-agent systems (MAS). We interpret the formulae of the logic over models generated by weighted deontic interpreted systems (WDIS). Furthermore, we investigate a SAT-based bounded model checking (BMC) technique for WDIS and for WECTL*KD.

DOI: 10.3233/FI-2016-1310

Journal: Fundamenta Informaticae, vol. 143, no. 1-2, pp. 173-205, 2016