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

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov

Research output: Contribution to journalConference article

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 Dec 1
EventCOTIC '98, Second Workshop on Concurrent Constraint Programming for Time Critical Applications and Multi-Agent Systems - Nice, France
Duration: 1998 Sep 71998 Sep 7

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this