Strong Completeness for Markovian Logics

Dexter Kozen; Radu Iulian Mardare; Prakash Panangaden

doi:10.1007/978-3-642-40313-2_58

Strong Completeness for Markovian Logics

Dexter Kozen, Radu Iulian Mardare, Prakash Panangaden

Department of Computer Science

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

11 Citations (Scopus)

Abstract

In this paper we present Hilbert-style axiomatizations for three logics for reasoning about continuous-space Markov processes (MPs): (i) a logic for MPs defined for probability distributions on measurable state spaces, (ii) a logic for MPs defined for sub-probability distributions and (iii) a logic defined for arbitrary distributions. These logics are not compact so one needs infinitary rules in order to obtain strong completeness results.

We propose a new infinitary rule that replaces the so-called Countable Additivity Rule (CAR) currently used in the literature to address the problem of proving strong completeness for these and similar logics. Unlike the CAR, our rule has a countable set of instances; consequently it allows us to apply the Rasiowa-Sikorski lemma for establishing strong completeness. Our proof method is novel and it can be used for other logics as well.

Original language	English
Title of host publication	Mathematical Foundations of Computer Science 2013 : 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings
Editors	Krishnendu Chatterjee , Jirí Sgall
Number of pages	12
Volume	LNCS 8087
Publisher	Springer Publishing Company
Publication date	2013
Pages	655-666
ISBN (Print)	978-3-642-40312-5
ISBN (Electronic)	978-3-642-40313-2
DOIs	https://doi.org/10.1007/978-3-642-40313-2_58
Publication status	Published - 2013
Event	38th International Symposium on Mathematical Foundations of Computer Science - IST Austria, Klosterneuburg, Austria Duration: 26 Aug 2013 → 30 Aug 2013 Conference number: 38th

Conference

Conference	38th International Symposium on Mathematical Foundations of Computer Science
Number	38th
Location	IST Austria
Country/Territory	Austria
City	Klosterneuburg
Period	26/08/2013 → 30/08/2013

Series	Lecture Notes in Computer Science
Volume	8087
ISSN	0302-9743

Access to Document

10.1007/978-3-642-40313-2_58

http://link.springer.com/chapter/10.1007/978-3-642-40313-2_58

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

Kozen, D., Mardare, R. I., & Panangaden, P. (2013). Strong Completeness for Markovian Logics. In K. Chatterjee , & J. Sgall (Eds.), Mathematical Foundations of Computer Science 2013: 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings (Vol. LNCS 8087, pp. 655-666). Springer Publishing Company. https://doi.org/10.1007/978-3-642-40313-2_58

Kozen, Dexter ; Mardare, Radu Iulian ; Panangaden, Prakash. / Strong Completeness for Markovian Logics. Mathematical Foundations of Computer Science 2013: 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings. editor / Krishnendu Chatterjee ; Jirí Sgall. Vol. LNCS 8087 Springer Publishing Company, 2013. pp. 655-666 (Lecture Notes in Computer Science, Vol. 8087).

@inproceedings{57de560c4cce4d1bb4107a06c4aefd83,

title = "Strong Completeness for Markovian Logics",

abstract = "In this paper we present Hilbert-style axiomatizations for three logics for reasoning about continuous-space Markov processes (MPs): (i) a logic for MPs defined for probability distributions on measurable state spaces, (ii) a logic for MPs defined for sub-probability distributions and (iii) a logic defined for arbitrary distributions. These logics are not compact so one needs infinitary rules in order to obtain strong completeness results.We propose a new infinitary rule that replaces the so-called Countable Additivity Rule (CAR) currently used in the literature to address the problem of proving strong completeness for these and similar logics. Unlike the CAR, our rule has a countable set of instances; consequently it allows us to apply the Rasiowa-Sikorski lemma for establishing strong completeness. Our proof method is novel and it can be used for other logics as well.",

author = "Dexter Kozen and Mardare, {Radu Iulian} and Prakash Panangaden",

year = "2013",

doi = "10.1007/978-3-642-40313-2_58",

language = "English",

isbn = "978-3-642-40312-5",

volume = "LNCS 8087",

series = "Lecture Notes in Computer Science",

publisher = "Springer Publishing Company",

pages = "655--666",

editor = "{Chatterjee }, Krishnendu and Jir{\'i} Sgall",

booktitle = "Mathematical Foundations of Computer Science 2013",

address = "United States",

note = "38th International Symposium on Mathematical Foundations of Computer Science, MFCS 2013 ; Conference date: 26-08-2013 Through 30-08-2013",

}

Kozen, D, Mardare, RI & Panangaden, P 2013, Strong Completeness for Markovian Logics. in K Chatterjee & J Sgall (eds), Mathematical Foundations of Computer Science 2013: 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings. vol. LNCS 8087, Springer Publishing Company, Lecture Notes in Computer Science, vol. 8087, pp. 655-666, 38th International Symposium on Mathematical Foundations of Computer Science, Klosterneuburg, Austria, 26/08/2013. https://doi.org/10.1007/978-3-642-40313-2_58

Strong Completeness for Markovian Logics. / Kozen, Dexter; Mardare, Radu Iulian; Panangaden, Prakash.
Mathematical Foundations of Computer Science 2013: 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings. ed. / Krishnendu Chatterjee ; Jirí Sgall. Vol. LNCS 8087 Springer Publishing Company, 2013. p. 655-666 (Lecture Notes in Computer Science, Vol. 8087).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

TY - GEN

T1 - Strong Completeness for Markovian Logics

AU - Kozen, Dexter

AU - Mardare, Radu Iulian

AU - Panangaden, Prakash

N1 - Conference code: 38th

PY - 2013

Y1 - 2013

N2 - In this paper we present Hilbert-style axiomatizations for three logics for reasoning about continuous-space Markov processes (MPs): (i) a logic for MPs defined for probability distributions on measurable state spaces, (ii) a logic for MPs defined for sub-probability distributions and (iii) a logic defined for arbitrary distributions. These logics are not compact so one needs infinitary rules in order to obtain strong completeness results.We propose a new infinitary rule that replaces the so-called Countable Additivity Rule (CAR) currently used in the literature to address the problem of proving strong completeness for these and similar logics. Unlike the CAR, our rule has a countable set of instances; consequently it allows us to apply the Rasiowa-Sikorski lemma for establishing strong completeness. Our proof method is novel and it can be used for other logics as well.

AB - In this paper we present Hilbert-style axiomatizations for three logics for reasoning about continuous-space Markov processes (MPs): (i) a logic for MPs defined for probability distributions on measurable state spaces, (ii) a logic for MPs defined for sub-probability distributions and (iii) a logic defined for arbitrary distributions. These logics are not compact so one needs infinitary rules in order to obtain strong completeness results.We propose a new infinitary rule that replaces the so-called Countable Additivity Rule (CAR) currently used in the literature to address the problem of proving strong completeness for these and similar logics. Unlike the CAR, our rule has a countable set of instances; consequently it allows us to apply the Rasiowa-Sikorski lemma for establishing strong completeness. Our proof method is novel and it can be used for other logics as well.

U2 - 10.1007/978-3-642-40313-2_58

DO - 10.1007/978-3-642-40313-2_58

M3 - Article in proceeding

SN - 978-3-642-40312-5

VL - LNCS 8087

T3 - Lecture Notes in Computer Science

SP - 655

EP - 666

BT - Mathematical Foundations of Computer Science 2013

A2 - Chatterjee , Krishnendu

A2 - Sgall, Jirí

PB - Springer Publishing Company

T2 - 38th International Symposium on Mathematical Foundations of Computer Science

Y2 - 26 August 2013 through 30 August 2013

ER -

Kozen D, Mardare RI, Panangaden P. Strong Completeness for Markovian Logics. In Chatterjee K, Sgall J, editors, Mathematical Foundations of Computer Science 2013: 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings. Vol. LNCS 8087. Springer Publishing Company. 2013. p. 655-666. (Lecture Notes in Computer Science, Vol. 8087). doi: 10.1007/978-3-642-40313-2_58

Strong Completeness for Markovian Logics

Abstract

Conference

Access to Document

AUB Link

Fingerprint

Cite this