A computer method of finding valuations forcing validity of LC formulae

Łukasz Godlewski; Kordula Świętorzecka; Jan Mulawka

doi:10.1117/12.2075115

2 December 2014 A computer method of finding valuations forcing validity of LC formulae

Łukasz Godlewski, Kordula Świętorzecka, Jan Mulawka

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.

Citation Download Citation

Łukasz Godlewski, Kordula Świętorzecka, and 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); https://doi.org/10.1117/12.2075115

ACCESS THE FULL ARTICLE

INSTITUTIONAL
Select your institution to access the SPIE Digital Library.

SELECT YOUR INSTITUTION

PERSONAL
Sign in with your SPIE account to access your personal subscriptions or to use specific features such as save to my library, sign up for alerts, save searches, etc.

PERSONAL SIGN IN

No SPIE Account? Create one

PURCHASE THIS CONTENT

SUBSCRIBE TO DIGITAL LIBRARY

50 downloads per 1-year subscription

Members: $195

Non-members: $335 ADD TO CART

25 downloads per 1 - year subscription

Members: $145

Non-members: $250 ADD TO CART

PURCHASE SINGLE ARTICLE

Includes PDF, HTML & Video, when available