2 December 2014 A computer method of finding valuations forcing validity of LC formulae
Author Affiliations +
Proceedings Volume 9290, Photonics Applications in Astronomy, Communications, Industry, and High-Energy Physics Experiments 2014; 92902X (2014) https://doi.org/10.1117/12.2075115
Event: Symposium on Photonics Applications in Astronomy, Communications, Industry and High-Energy Physics Experiments, 2014, Warsaw, Poland
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.
© (2014) COPYRIGHT Society of Photo-Optical Instrumentation Engineers (SPIE). Downloading of the abstract is permitted for personal use only.
Łukasz Godlewski, Kordula Świętorzecka, Jan Mulawka, "A computer method of finding valuations forcing validity of LC formulae", Proc. SPIE 9290, Photonics Applications in Astronomy, Communications, Industry, and High-Energy Physics Experiments 2014, 92902X (2 December 2014); doi: 10.1117/12.2075115; https://doi.org/10.1117/12.2075115
PROCEEDINGS
10 PAGES


SHARE
RELATED CONTENT


Back to Top