Concurrent weighted logic

•We introduce Concurrent Weighted Logic for concurrent labeled weighted systems.•We develop a weak- and strong-complete axiomatic system.•We prove an extension of Rasiowa–Sikorski lemma to demonstrate Lindenbaum's lemma.

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.