Model Checking and Synthesis for Branching Multi-Weighted Logics

JENSEN, Lasse S., Isabella KAUFMANN, Kim G. LARSEN, Soeren M. NIELSEN and Jiří SRBA. Model Checking and Synthesis for Branching Multi-Weighted Logics. Journal of Logical and Algebraic Methods in Programming. 2019, vol. 105, June 2019, p. 28-46. ISSN 2352-2208. Available from: https://dx.doi.org/10.1016/j.jlamp.2019.02.001.

Basic information

• Original name: Model Checking and Synthesis for Branching Multi-Weighted Logics
• Authors: JENSEN, Lasse S. (208 Denmark), Isabella KAUFMANN (208 Denmark), Kim G. LARSEN (208 Denmark), Soeren M. NIELSEN (208 Denmark) and Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution).
• Edition: Journal of Logical and Algebraic Methods in Programming, 2019, 2352-2208.

Other information

• Original language: English
• Type of outcome: Article in a journal
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Netherlands
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• Impact factor: Impact factor: 0.685
• RIV identification code: RIV/00216224:14330/19:00113645
• Organization unit: Faculty of Informatics
• Doi: http://dx.doi.org/10.1016/j.jlamp.2019.02.001
• UT WoS: 000467670900002
• Keywords in English: model checking; logic; synthesis

Abstract

We investigate the open synthesis problem in a quantitative game theoretic setting where the system model is annotated with multiple nonnegative weights representing quantitative resources such as energy, discrete time or cost. We consider system specifications expressed in the branching time logic CTL extended with bounds on resources. As our first contribution, we show that the model checking problem for the full logic is undecidable with already three weights. By restricting the bounds to constant upper or lower-bounds on the individual weights, we demonstrate that the problem becomes decidable and that the model checking problem is PSPACE-complete. As a second contribution, we show that by imposing upper-bounds on the temporal operators and assuming that the cost converges over infinite runs, the synthesis problem is also decidable. Finally, we provide an on-the-fly algorithm for the synthesis problem on an unrestricted model for a reachability fragment of the logic and we prove EXPTIME-completeness of the synthesis problem.