TY - JOUR
T1 - Concurrent weighted logic
AU - Xue, Bingtian
AU - Larsen, Kim Guldstrand
AU - Mardare, Radu Iulian
PY - 2015
Y1 - 2015
N2 - We introduce Concurrent Weighted Logic (CWL), a multimodal logic for concurrent labeled weighted transition systems (LWSs). The synchronization of LWSs is described using dedicated functions that, in various concurrency paradigms, allow us to encode the compositionality of LWSs. To reflect these, CWL contains modal operators indexed with rational numbers to predicate over the numerical labels of LWSs as well as a binary modal operator that encodes properties concerning the (de-) composition of LWSs. We develop a Hilbert-style axiomatic system for CWL and we prove weak- and strong-completeness results for this logic. To complete these proofs we involve advanced topological techniques from Model Theory.
AB - We introduce Concurrent Weighted Logic (CWL), a multimodal logic for concurrent labeled weighted transition systems (LWSs). The synchronization of LWSs is described using dedicated functions that, in various concurrency paradigms, allow us to encode the compositionality of LWSs. To reflect these, CWL contains modal operators indexed with rational numbers to predicate over the numerical labels of LWSs as well as a binary modal operator that encodes properties concerning the (de-) composition of LWSs. We develop a Hilbert-style axiomatic system for CWL and we prove weak- and strong-completeness results for this logic. To complete these proofs we involve advanced topological techniques from Model Theory.
KW - Non-compact modal logic
KW - Model theory
KW - Rasiowa–Sikorski lemma
KW - Weighted transition systems
KW - Concurrency
U2 - 10.1016/j.jlamp.2015.07.002
DO - 10.1016/j.jlamp.2015.07.002
M3 - Journal article
SN - 2352-2208
VL - 84
SP - 884
EP - 897
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
IS - 6
ER -