Share Email Print
cover

Proceedings Paper

A computer method of finding valuations forcing validity of LC formulae
Author(s): Łukasz Godlewski; Kordula Świętorzecka; Jan Mulawka
Format Member Price Non-Member Price
PDF $14.40 $18.00
cover GOOD NEWS! Your organization subscribes to the SPIE Digital Library. You may be able to download this paper for free. Check Access

Paper Abstract

The purpose of this paper is to present the computer implementation of a system known as LC temporal logic [1]. Firstly, to become familiar with some theoretical issues, a short introduction to this logic is discussed. The algorithms allowing a deep analysis of the formulae of LC logic are considered. In particular we discuss how to determine if a formula is a tautology, contrtautology or it is satisfable. Next, we show how to find all valuations to satisfy the formula. Finally, we consider finding histories generated by the formula and transforming these histories into the state machine. Moreover, a description of the experiments that verify the implementation are briefly presented.

Paper Details

Date Published: 2 December 2014
PDF: 10 pages
Proc. SPIE 9290, Photonics Applications in Astronomy, Communications, Industry, and High-Energy Physics Experiments 2014, 92902X (2 December 2014); doi: 10.1117/12.2075115
Show Author Affiliations
Łukasz Godlewski, Warsaw Univ. of Technology (Poland)
Kordula Świętorzecka, Cardinal Stefan Wyszynski Univ. (Poland)
Jan Mulawka, Warsaw Univ. of Technology (Poland)


Published in SPIE Proceedings Vol. 9290:
Photonics Applications in Astronomy, Communications, Industry, and High-Energy Physics Experiments 2014
Ryszard S. Romaniuk, Editor(s)

© SPIE. Terms of Use
Back to Top