Concurrent weighted logic

Kim G. Larsen; Radu Mardare; Bingtian Xue

doi:10.1016/j.jlamp.2015.07.002

Concurrent weighted logic

Kim G. Larsen, Radu Mardare, Bingtian Xue

Computer And Information Sciences

Research output: Contribution to journal › Article › peer-review

2 Citations (Scopus)

Abstract

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.

Original language	English
Pages (from-to)	884-897
Number of pages	14
Journal	Journal of Logical and Algebraic Methods in Programming
Volume	84
Issue number	6
Early online date	17 Jul 2015
DOIs	https://doi.org/10.1016/j.jlamp.2015.07.002
Publication status	Published - 30 Nov 2015

Keywords

non-compact modal logic
model theory
Rasiowa–Sikorski lemma
weighted transition systems
concurrency

Access to Document

10.1016/j.jlamp.2015.07.002

Cite this

@article{717bf7f329b74ece87e49aae3ddf0215,

title = "Concurrent weighted logic",

abstract = "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.",

keywords = "non-compact modal logic, model theory, Rasiowa–Sikorski lemma, weighted transition systems, concurrency",

author = "Larsen, \{Kim G.\} and Radu Mardare and Bingtian Xue",

year = "2015",

month = nov,

day = "30",

doi = "10.1016/j.jlamp.2015.07.002",

language = "English",

volume = "84",

pages = "884--897",

journal = "Journal of Logical and Algebraic Methods in Programming",

issn = "2352-2208",

publisher = "Elsevier Inc.",

number = "6",

}

TY - JOUR

T1 - Concurrent weighted logic

AU - Larsen, Kim G.

AU - Mardare, Radu

AU - Xue, Bingtian

PY - 2015/11/30

Y1 - 2015/11/30

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 - 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 -

Concurrent weighted logic

Abstract

Keywords

Access to Document

Fingerprint

Cite this