Linear time-dependent constraints programming with MSVL (Q2015809)

The paper is concerned with specifying and solving linear time-dependent constraints with MSVL. In particular, the focus is on linear equalities and strict inequalities. The main contributions of the paper are the following: {\parindent=6mm \begin{itemize}\item[1.] Linear constraint statements are defined within the specification language of MSVL. \item[2.] Operational semantics for linear constraints are provided. \item[3.] The soundness of the operational rules for linear constraints is rigorously established. \end{itemize}} The authors did a thorough job of explaining the problem that they study and of deriving the appropriate results. The paper itself is a good addition to the overall literature in the fields of program semantics and formal verification. The paper is well-written. There are a few places where articles (such as ``the'') are used incorrectly, but on the whole the exposition is good. The discussion on related work is thorough. The authors describe (albeit briefly) all the major advances in the field of logic programming and in particular temporal logic programming. I could not discover any error in the proofs given in the paper and the work is clearly original. The contributions made by the authors are well-laid-out and clear. Using MSVL to capture linear constraints was not known prior to their work. They also plan to combine their techniques with common SMT solvers. It follows that their work is original and impressive.