Specifying real-time finite-state systems in linear logic (extended abstract)

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov

Research output: Contribution to journalArticle

8 Citations (Scopus)

Abstract

Real-time finite-state systems may be specified in linear logic by means of linear implications between conjunctions of fixed finite length. In this setting, where time is treated as a dense linear ordering, safety properties may be expressed as certain provability problems. These provability problems are shown to be in PSPACE. They are solvable, with some guidance, by finite proof search in concurrent logic programming environments based on linear logic and acting as sort of model-checkers. One advantage of our approach is that either it provides unsafe runs or it actually establishes safety.

Original languageEnglish
Pages (from-to)42-59
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Volume16
Issue number1
DOIs
Publication statusPublished - 1998

Fingerprint

Linear Logic
Real-time
Logic programming
Safety
Proof Search
Concurrent Programming
Linear Ordering
Programming Environments
Logic Programming
Sort
Guidance
Model

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Specifying real-time finite-state systems in linear logic (extended abstract). / Kanovich, Max I.; Okada, Mitsuhiro; Scedrov, Andre.

In: Electronic Notes in Theoretical Computer Science, Vol. 16, No. 1, 1998, p. 42-59.

Research output: Contribution to journalArticle

@article{e4199b8dea454b718cb410d9e0f25fe5,
title = "Specifying real-time finite-state systems in linear logic (extended abstract)",
abstract = "Real-time finite-state systems may be specified in linear logic by means of linear implications between conjunctions of fixed finite length. In this setting, where time is treated as a dense linear ordering, safety properties may be expressed as certain provability problems. These provability problems are shown to be in PSPACE. They are solvable, with some guidance, by finite proof search in concurrent logic programming environments based on linear logic and acting as sort of model-checkers. One advantage of our approach is that either it provides unsafe runs or it actually establishes safety.",
author = "Kanovich, {Max I.} and Mitsuhiro Okada and Andre Scedrov",
year = "1998",
doi = "10.1016/S1571-0661(05)80591-2",
language = "English",
volume = "16",
pages = "42--59",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "1",

}

TY - JOUR

T1 - Specifying real-time finite-state systems in linear logic (extended abstract)

AU - Kanovich, Max I.

AU - Okada, Mitsuhiro

AU - Scedrov, Andre

PY - 1998

Y1 - 1998

N2 - Real-time finite-state systems may be specified in linear logic by means of linear implications between conjunctions of fixed finite length. In this setting, where time is treated as a dense linear ordering, safety properties may be expressed as certain provability problems. These provability problems are shown to be in PSPACE. They are solvable, with some guidance, by finite proof search in concurrent logic programming environments based on linear logic and acting as sort of model-checkers. One advantage of our approach is that either it provides unsafe runs or it actually establishes safety.

AB - Real-time finite-state systems may be specified in linear logic by means of linear implications between conjunctions of fixed finite length. In this setting, where time is treated as a dense linear ordering, safety properties may be expressed as certain provability problems. These provability problems are shown to be in PSPACE. They are solvable, with some guidance, by finite proof search in concurrent logic programming environments based on linear logic and acting as sort of model-checkers. One advantage of our approach is that either it provides unsafe runs or it actually establishes safety.

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

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

U2 - 10.1016/S1571-0661(05)80591-2

DO - 10.1016/S1571-0661(05)80591-2

M3 - Article

AN - SCOPUS:0038245727

VL - 16

SP - 42

EP - 59

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 1

ER -