Title :
Integration of Linear Constraints with a Temporal Logic Programming Language
Author :
Qian Ma ; Zhenhua Duan ; Mengfei Yang
Author_Institution :
Inst. of Comput. Theor. & Technol., Xidian Univ., Xi´an, China
Abstract :
This paper investigates the integration of linear constraints with MSVL. To this end, we first define linear constraint statements and discuss related issues of the incorporation. Further, for calling SMT solvers to solve the newly introduced constraints, we give a translation algorithm from state programs in MSVL with linear constraints to SMT-LIB2.0 script language and then supply a solving procedure.
Keywords :
authoring languages; logic programming languages; temporal logic; MSVL; SMT solvers; SMT-LIB2.0 script language; linear constraints; state programs; temporal logic programming language; Arrays; Logic programming; Noise measurement; Optimization; Semantics; Syntactics;
Conference_Titel :
Theoretical Aspects of Software Engineering (TASE), 2013 International Symposium on
Conference_Location :
Birmingham
DOI :
10.1109/TASE.2013.30
