TY - GEN
T1 - A decidable recursive logic forweighted transition systems
AU - Larsen, Kim Guldstrand
AU - Mardare, Radu
AU - Xue, Bingtian
PY - 2014/9/23
Y1 - 2014/9/23
N2 - In this paper we develop and study the Recursive Weighted Logic (RWL), a multi-modal logic that expresses qualitative and quantitative properties of labelled weighted transition systems (LWSs). LWSs are transition systems labelled with actions and real-valued quantities representing the costs of transitions with respect to various resources. RWL uses first-order variables to measure local costs. The main syntactic operators are similar to the ones of timed logics for real-time systems. In addition, our logic is endowed, with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We prove that unlike in the case of the timed logics, the satisfiability problem for RWL is decidable. The proof uses a variant of the region construction technique used in literature with timed automata, which we adapt to the specific settings of RWL. This paper extends previous results that we have demonstrated for a similar but much more restrictive logic that can only use one variable for each type of resource to encode logical properties.
AB - In this paper we develop and study the Recursive Weighted Logic (RWL), a multi-modal logic that expresses qualitative and quantitative properties of labelled weighted transition systems (LWSs). LWSs are transition systems labelled with actions and real-valued quantities representing the costs of transitions with respect to various resources. RWL uses first-order variables to measure local costs. The main syntactic operators are similar to the ones of timed logics for real-time systems. In addition, our logic is endowed, with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We prove that unlike in the case of the timed logics, the satisfiability problem for RWL is decidable. The proof uses a variant of the region construction technique used in literature with timed automata, which we adapt to the specific settings of RWL. This paper extends previous results that we have demonstrated for a similar but much more restrictive logic that can only use one variable for each type of resource to encode logical properties.
KW - labelled weighted transition system
KW - maximal fixed point computation
KW - multi-modal logic
UR - http://www.scopus.com/inward/record.url?scp=84921790649&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-10882-7_27
DO - 10.1007/978-3-319-10882-7_27
M3 - Conference contribution book
AN - SCOPUS:84921790649
SN - 9783319108810
SN - 9783319108827
T3 - Lecture Notes in Computer Science
SP - 460
EP - 476
BT - Theoretical Aspects of Computing – ICTAC 2014
A2 - Ciobanu, Gabriel
A2 - Méry, Dominique
PB - Springer
CY - Cham
ER -