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

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov

Research output: Contribution to journalConference articlepeer-review

9 Citations (Scopus)


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
Issue number1
Publication statusPublished - 1998
Externally publishedYes
EventCOTIC '98, Second Workshop on Concurrent Constraint Programming for Time Critical Applications and Multi-Agent Systems - Nice, France
Duration: 1998 Sept 71998 Sept 7

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Specifying real-time finite-state systems in linear logic (extended abstract)'. Together they form a unique fingerprint.

Cite this