Semantics for "enough-certainty" and fitting's embedding of classical logic in S4

Gergei Bana, Mitsuhiro Okada

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In this work we look at how Fitting's embedding of first-order classical logic into first-order S4 can help in reasoning when we are interested in satisfaction "in most cases", when first-order properties are allowed to fail in cases that are considered insignificant. We extend classical semantics by combining a Kripke-style model construction of "significant" events as possible worlds with the forcing-Fitting-style semantics construction by embedding classical logic into S4. We provide various examples. Our main running example is an application to symbolic security protocol verification with complexity-theoretic guarantees. In particular, we show how Fitting's embedding emerges entirely naturally when verifying trace properties in computer security.

Original languageEnglish
Title of host publicationComputer Science Logic 2016, CSL 2016
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volume62
ISBN (Electronic)9783959770224
DOIs
Publication statusPublished - 2016 Aug 1
Event25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic - Marseille, France
Duration: 2016 Aug 292016 Sep 1

Other

Other25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic
CountryFrance
CityMarseille
Period16/8/2916/9/1

Fingerprint

Semantics
Security of data
Network protocols

Keywords

  • Asymptotic probabilities
  • First-order logic
  • Fitting embedding
  • Possible-world semantics
  • Verification of complexity-theoretic properties

ASJC Scopus subject areas

  • Software

Cite this

Bana, G., & Okada, M. (2016). Semantics for "enough-certainty" and fitting's embedding of classical logic in S4. In Computer Science Logic 2016, CSL 2016 (Vol. 62). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2016.34

Semantics for "enough-certainty" and fitting's embedding of classical logic in S4. / Bana, Gergei; Okada, Mitsuhiro.

Computer Science Logic 2016, CSL 2016. Vol. 62 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2016.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Bana, G & Okada, M 2016, Semantics for "enough-certainty" and fitting's embedding of classical logic in S4. in Computer Science Logic 2016, CSL 2016. vol. 62, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic, Marseille, France, 16/8/29. https://doi.org/10.4230/LIPIcs.CSL.2016.34
Bana G, Okada M. Semantics for "enough-certainty" and fitting's embedding of classical logic in S4. In Computer Science Logic 2016, CSL 2016. Vol. 62. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2016 https://doi.org/10.4230/LIPIcs.CSL.2016.34
Bana, Gergei ; Okada, Mitsuhiro. / Semantics for "enough-certainty" and fitting's embedding of classical logic in S4. Computer Science Logic 2016, CSL 2016. Vol. 62 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2016.
@inproceedings{556c0f9d187b446d9855b36d304a256a,
title = "Semantics for {"}enough-certainty{"} and fitting's embedding of classical logic in S4",
abstract = "In this work we look at how Fitting's embedding of first-order classical logic into first-order S4 can help in reasoning when we are interested in satisfaction {"}in most cases{"}, when first-order properties are allowed to fail in cases that are considered insignificant. We extend classical semantics by combining a Kripke-style model construction of {"}significant{"} events as possible worlds with the forcing-Fitting-style semantics construction by embedding classical logic into S4. We provide various examples. Our main running example is an application to symbolic security protocol verification with complexity-theoretic guarantees. In particular, we show how Fitting's embedding emerges entirely naturally when verifying trace properties in computer security.",
keywords = "Asymptotic probabilities, First-order logic, Fitting embedding, Possible-world semantics, Verification of complexity-theoretic properties",
author = "Gergei Bana and Mitsuhiro Okada",
year = "2016",
month = "8",
day = "1",
doi = "10.4230/LIPIcs.CSL.2016.34",
language = "English",
volume = "62",
booktitle = "Computer Science Logic 2016, CSL 2016",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

}

TY - GEN

T1 - Semantics for "enough-certainty" and fitting's embedding of classical logic in S4

AU - Bana, Gergei

AU - Okada, Mitsuhiro

PY - 2016/8/1

Y1 - 2016/8/1

N2 - In this work we look at how Fitting's embedding of first-order classical logic into first-order S4 can help in reasoning when we are interested in satisfaction "in most cases", when first-order properties are allowed to fail in cases that are considered insignificant. We extend classical semantics by combining a Kripke-style model construction of "significant" events as possible worlds with the forcing-Fitting-style semantics construction by embedding classical logic into S4. We provide various examples. Our main running example is an application to symbolic security protocol verification with complexity-theoretic guarantees. In particular, we show how Fitting's embedding emerges entirely naturally when verifying trace properties in computer security.

AB - In this work we look at how Fitting's embedding of first-order classical logic into first-order S4 can help in reasoning when we are interested in satisfaction "in most cases", when first-order properties are allowed to fail in cases that are considered insignificant. We extend classical semantics by combining a Kripke-style model construction of "significant" events as possible worlds with the forcing-Fitting-style semantics construction by embedding classical logic into S4. We provide various examples. Our main running example is an application to symbolic security protocol verification with complexity-theoretic guarantees. In particular, we show how Fitting's embedding emerges entirely naturally when verifying trace properties in computer security.

KW - Asymptotic probabilities

KW - First-order logic

KW - Fitting embedding

KW - Possible-world semantics

KW - Verification of complexity-theoretic properties

UR - http://www.scopus.com/inward/record.url?scp=85012865578&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85012865578&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CSL.2016.34

DO - 10.4230/LIPIcs.CSL.2016.34

M3 - Conference contribution

AN - SCOPUS:85012865578

VL - 62

BT - Computer Science Logic 2016, CSL 2016

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

ER -