• DocumentCode
    3022079
  • 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
  • fYear
    2013
  • fDate
    1-3 July 2013
  • Firstpage
    157
  • Lastpage
    164
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Theoretical Aspects of Software Engineering (TASE), 2013 International Symposium on
  • Conference_Location
    Birmingham
  • Type

    conf

  • DOI
    10.1109/TASE.2013.30
  • Filename
    6597893
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3022079