[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content

Advertisement

Springer Nature Link
Log in

Linear time-dependent constraints programming with MSVL

  • Published:
Journal of Combinatorial Optimization Aims and scope Submit manuscript

Abstract

This paper investigates specifying and solving linear time-dependent constraints with an interval temporal logic programming language MSVL. To this end, linear constraint statements involving linear equality and non-strict inequality are first defined. Further, the time-dependent relations in the constraints are specified by temporal operators, such as . Thus, linear time-dependent constraints can be smoothly incorporated into MSVL. Moreover, to solve the linear constraints within MSVL by means of reduction, the operational semantics for linear constraints is given. In particular, semantic equivalence rules and transition rules within a state are presented, which enable us to reduce linear equations, inequalities and optimization problems in a convenient way. Besides, the operational semantics is proved to be sound. Finally, a production scheduling application is provided to illustrate how our approach works in practice.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4

Similar content being viewed by others

References

  • Allen JF (1983) Maintaining knowledge about temporal intervals. Commun ACM 26(11):832–843

    Article  MATH  Google Scholar 

  • Analyti A, Pachoulakis I (2012) Temporally annotated extended logic programs. Int J Res Rev Artif Intell 2(1):107–112

    Google Scholar 

  • Baldan P, Mancarella P, Raffaetà A, Turini F (2002) Mutaclp: a language for temporal reasoning with multiple theories. In: Proceedings of computational logic: logic programming and beyond, pp 1–40

    Chapter  Google Scholar 

  • Barrett C, Deters M, Oliveras A, Stump A (2008) Design and results of the 3rd annual satisfiability modulo theories competition (SMT-COMP). Int J Artif Intell 17:569–606

    Article  Google Scholar 

  • Barrett C, Stump A, Tinelli C (2010) The SMT-LIB standard: version 2.0. In: Proceedings of the 8th international workshop on satisfiability modulo theories

    Google Scholar 

  • Barringer H, Fisher M, Gabbay D, Gough G, Owens R (1990) Metatem: a framework for programming in temporal logic. In: REX workshop on stepwise refinement of distributed systems: models, formalisms, correctness. LNCS, vol 430. Springer, Berlin, pp 94–129

    Chapter  Google Scholar 

  • Berry G, Gonthier G (1992) The ESTEREL synchronous programming language: design, semantics, implementation. Sci Comput Program 19(2):87–152

    Article  MATH  Google Scholar 

  • Brailsford SC, Potts CN, Smith BM (1999) Constraint satisfaction problems: algorithms and applications. Eur J Oper Res 119:557–581

    Article  MATH  Google Scholar 

  • Brzoska C (1998) Programming in metric temporal logic. Theor Comput Sci 202(1–2):55–125

    Article  MATH  MathSciNet  Google Scholar 

  • Cormen TH, Leiserson CE, Rivest RL, Stein C (2005) Introduction to algorithms. MIT Press, Cambridge

    Google Scholar 

  • Dantzig GB, Orden A, Wolfe P (1955) The generalized simplex method for minimizing a linear form under linear inequality constraints. Pac J Math 50(2):183–195

    Article  MathSciNet  Google Scholar 

  • Dechter R, Meiri I, Pearl J (1991) Temporal constraint networks. Artif Intell 49(1–3):61–95

    Article  MATH  MathSciNet  Google Scholar 

  • Duan Z (1996) An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis, University of Newcastle Upon Tyne

  • Duan Z (2006) Temporal logic and temporal logic programming language. Science Press, Beijing

    Google Scholar 

  • Duan Z, Tian C (2008) A unified model checking approach with projection temporal logic. In: Proceedings of ICFEM08, pp 167–186

    Google Scholar 

  • Duan Z, Yang C (2010) Unconditional secure communication: a Russian cards protocol. J Comb Optim 19(4):501–530

    Article  MATH  MathSciNet  Google Scholar 

  • Duan Z, Koutny M, Holt C (1994) Projection in temporal logic programming. In: Proceedings of logic programming and automated reasoning. LNAI, vol 822, pp 333–344

    Chapter  Google Scholar 

  • Duan Z, Yang X, Koutny M (2008) Framed temporal logic programming. Sci Comput Program 70:31–61

    Article  MATH  MathSciNet  Google Scholar 

  • Frühwirth TW (1994) Annotated constraint logic programming applied to temporal reasoning. In: Proceedings of programming language implementation and logic programming 94. LNCS, vol 844, pp 230–243

    Chapter  Google Scholar 

  • Frühwirth TW (1996) Temporal annotated constraint logic programming. J Symb Comput 22(5/6):555–583

    Article  MATH  Google Scholar 

  • Fujita M, Kono S, Tanaka H, Moto-oka T (1986) Tokio: logic programming language based on temporal logic and its compilation to Prolog. In: Proceedings of ICLP86. LNCS, vol 225. Springer, Berlin, pp 695–709

    Google Scholar 

  • Gupta V, Jagadeesan R, Saraswat VA (1998) Computing with continuous change. Sci Comput Program 30(1–2):3–49

    Article  MATH  MathSciNet  Google Scholar 

  • Hentenryck PV (1989) Constraint satisfaction in logic programming. MIT Press, Cambridge

    Google Scholar 

  • Hrycej T (1988) Temporal Prolog. In: Proceedings of ECAI, vol 88, pp 296–301

    Google Scholar 

  • Jaffar J, Lassez JL (1987) Constraint logic programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on principles of programming languages. ACM, New York, pp 111–119

    Chapter  Google Scholar 

  • Lamport L (1994) The temporal logic of actions. ACM Trans Program Lang Syst 16(3):872–923

    Article  Google Scholar 

  • Lei L, Duan Z (2007) Automating web service composition for collaborative business processes. In: Proceedings of CSCWD07, pp 894–899

    Google Scholar 

  • Luca Bordeaux YH, Zhang L (2006) Propositional satisfiability and constraint programming: a comparative survey. ACM Comput Surv 38(4)

  • Ma Y, Duan Z, Wang X, Yang X (2007) An interpreter for framed Tempura and its application. In: Proceedings of TASE07, pp 251–260

    Google Scholar 

  • Manna Z, Pnueli A (1992) Temporal logic of reactive and concurrent systems. Springer, Berlin

    Book  Google Scholar 

  • Meiri I (1996) Combining qualitative and quantitative constraints in temporal reasoning. Artif Intell 87:343–385

    Article  MathSciNet  Google Scholar 

  • Moszkowski BC (1986) Executing temporal logic programs. PhD thesis, Cambridge University

  • Mouhoub M, Sukpan A (2012) Conditional and composite temporal csps. Appl Intell 36:90–107

    Article  Google Scholar 

  • Nielsen M, Palamidessi C, Valencia FD (2002) Temporal concurrent constraint programming: denotation, logic and applications. Nord J Comput 9:145–188

    MATH  MathSciNet  Google Scholar 

  • Saraswat V (1989) Concurrent constraint programming languages. PhD thesis, Carnegie-Mellon University

  • Saraswat VA, Jagadeesan R, Gupta V (1994) Foundations of timed concurrent constraint programming. In: Proceedings of the ninth annual IEEE symposium on logic in computer science, pp 71–80

    Chapter  Google Scholar 

  • Saraswat VA, Jagadeesan R, Gupta V (1996) Timed default concurrent constraint programming. J Symb Comput 22(5–6):475–520

    Article  MATH  MathSciNet  Google Scholar 

  • Sarria GM (2010) Improving the real-time concurrent constraint calculus with a delay declaration. In: Proceedings of WCECS10, pp 9–14

    Google Scholar 

  • Sarria GM, Rueda C (2008) Real-time concurrent constraint programming. In: Proceedings of CLEI08

    Google Scholar 

  • Tang CS (1983) Toward a unified logic basis for programming languages. In: Proceedings of IFIP congress. Elsevier, Amsterdam, pp 425–429

    Google Scholar 

  • Vilain M, Kautz H (1986) Constraint propagation algorithms for temporal reasoning. In: Proceedings of AAAI86, pp 377–382

    Google Scholar 

  • Yang X, Duan Z (2008) Operational semantics of framed tempura. J Log Algebr Program 78(1):22–51

    Article  MATH  MathSciNet  Google Scholar 

  • Yang X, Duan Z, Ma Q (2010) Axiomatic semantics of projection temporal logic programs. Math Struct Comput Sci 20(5):865–914

    Article  MATH  MathSciNet  Google Scholar 

  • Zhang N, Duan Z, Tian C (2012) A cylinder computation model for many-core parallel computing. Theor Comput Sci. doi:10.1016/j.tcs.2012.02.011

    MathSciNet  Google Scholar 

Download references

Acknowledgements

We appreciate the anonymous reviewers about their valuable comments and suggestions. We believe their meritorious advice will serve us well throughout our career.

Author information

Authors and Affiliations

  1. Institute of Computing Theory and Technology, Xidian University, P.O. Box 177, Xi’an, 710071, P.R. China

    Qian Ma & Zhenhua Duan

Authors
  1. Qian Ma
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhenhua Duan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhenhua Duan.

Additional information

This research is supported by the NSFC Grant Nos. 61133001, 60910004, 61272118, 61272117, 61202038, National Program on Key Basic Research Project (973 Program) Grant No. 2010CB328102.

Appendix

Appendix

1.1 The proof of Lemma 2

Proof

In Yang and Duan (2008), it has been proved that by using semantic equivalence rules in Figs. 6 and 7, any MSVL program q without linear constraints can be rewritten into an equivalent program q″ in the form of

$$q'' \equiv\bigvee\limits^{k}_{i=1} (q_{ei}\wedge \varepsilon ) \vee\bigvee\limits^{h}_{j=1} (q_{cj} \wedge\bigcirc q_{fj}) $$

such that q≡q″, where k+h≥1, q fj is a general program in MSVL whereas q ei and q cj are true or all state formulas of the form: \((x_{1} =c_{1}) \wedge\cdots\wedge(x_{l} =c_{l}) \wedge \dot{p}_{x_{1}} \wedge\cdots\wedge\dot{p}_{x_{l}}\) with c r ∈D (1≤r≤l) and \(\dot{p}_{x}\) denoting p x or ¬p x . Obviously, this form is a special instance of the normal form defined in Definition 8 with q mj ≡true. Let q′ be q″. Thus, the conclusion holds. □

1.2 The proof of Theorem 5

Proof

If q is an MSVL program without linear constraints, we can rewrite it into its normal form according to Lemma 2 by semantic equivalence rules in Figures 6 and 7. Then we only need to prove that for any linear constraint statement, it can be reduced into its normal form. The proof proceeds on the structure of the statements:

(a) If q is linear equality statement le 1=le 2, we have

$$\begin{array}{rcl@{\hspace{2.7cm}}r} \mathit {le}_1=\mathit {le}_2&\equiv& \mathit {le}_1=\mathit {le}_2 \wedge \mathsf {true}\\ &\equiv& \mathit {le}_1=\mathit {le}_2 \wedge(\varepsilon \vee\bigcirc \mathsf {true}) & (\mathsf {true}\equiv \varepsilon \vee \bigcirc \mathsf {true})\\ & \equiv& \mathit {le}_1=\mathit {le}_2 \wedge \varepsilon \vee \mathit {le}_1=\mathit {le}_2 \wedge \bigcirc \mathsf {true}&\mbox {(a1)}\\ \end{array} $$

In light of the definition of linear expressions, we discuss it in two cases:

(i) If either of le 1 and le 2 contains the temporal operator ◯, le 1=le 2∧ε≡false. Note that at the current state, the linear expression with can be evaluated into a constant by evaluation rules, so we treat such linear expression as a constant. By rules (Equ1, 2, 4) in Table 2 and (AEqu13) in Table 1, we can transpose all the temporal linear expressions to the left side with the next operator outmost and all the state linear expressions to the right side. After that, le 1=le 2 is rewritten into \(\bigcirc \mathit {le}_{1}'=\mathit {le}_{2}'\), where \(\mathit {le}_{1}'\) is a general linear expression while \(\mathit {le}_{2}'\) is a state linear expression. Thus, its normal form is

$$\begin{array}{l@{\hspace{1.8cm}}r} \mbox{(a1)}\equiv\bigcirc \mathit {le}_1'=\mathit {le}_2' \wedge\bigcirc \mathsf {true}& \mbox{(AEqu13 in Table 1, Equ1, 2, 4 in Table 2)} \end{array} $$

where the present component q cj is true.

(ii) Otherwise, neither of le 1 and le 2 contains the temporal operator. By (Equ1, 2) in Table 2 and laws in Table 1, le 1=le 2 can be rewritten into x=le′ by transposing all the expressions except variable x into the right side, so we obtain the normal form:

$$\begin{array}{l@{\hspace{2.5cm}}r} \mbox{(a1)}\equiv x=\mathit {le}' \wedge \varepsilon \vee x=\mathit {le}' \wedge\bigcirc \mathsf {true}& \hfill \mbox{(Table 1, Equ1, 2 in Table 2)}\\ \end{array} $$

(b) If q is c∗x⇐le, it can be reduced similarly as case (a).

(c) If q is LTET inequality statement le 1≤le 2, we have the following:

(i) If neither le 1 nor le 2 involves any temporal operators

$$\begin{array}{lll} \mathit {le}_1\leq \mathit {le}_2&\equiv& \exists x: x=\mathit {le}_2-\mathit {le}_1 \wedge x\geq 0\hfill \mbox{(InEqu5 in Table 3)}\\ & \stackrel {x}{\equiv }& x=\mathit {le}_2-le_1 \wedge x\geq0 \hfill \mbox{(InEqu5 in Table 3)}\\ &\equiv& x=\mathit {le}_2-\mathit {le}_1 \wedge0\leq x \wedge(\varepsilon \vee\bigcirc \mathsf {true})\qquad (\mbox{InEqu3 in Table 3, Fig.~7})\\ & \equiv& x=\mathit {le}_2-\mathit {le}_1 \wedge0\leq x \wedge \varepsilon \vee x=\mathit {le}_2-\mathit {le}_1 \wedge0\leq x \wedge\bigcirc \mathsf {true}\end{array} $$

Therefore, le 1≤le 2 has already in its normal form.

(ii) Otherwise, by using (InEqu1, 6, AEqu13), we transpose all the temporal linear expressions to the left side with the next operator outmost and all the state linear expressions to the right side. Then le 1≤le 2 is reduced into \(\bigcirc \mathit {le}_{1}'\leq \mathit {le}_{2}'\), where \(\mathit {le}_{1}'\) is a general linear expression while \(\mathit {le}_{2}'\) is a state linear expression. Further,

$$\begin{array}{l@{\hspace{1.4cm}}l} \mathit {le}_1\leq \mathit {le}_2 \equiv\bigcirc \mathit {le}_1'\leq \mathit {le}_2' \wedge\bigcirc \mathsf {true}&\mbox{(Figure 7, Table 1, InEqu1, 6 in Table 3) } \end{array} $$

Other composite statements can be transformed into their normal forms by first expanding their definitions and then their reductions come down to the basic cases above. For example, GTET statement le 1≥le 2 is rewritten as −le 1≤−le 2, which can be reduced into its normal form in case (c). □

1.3 Basic operational semantics of MSVL

The basic operational rules of MSVL in Yang and Duan (2008) are given below. In Fig. 5, evaluation rules of arithmetic expressions are presented by rules (A1–A5) while evaluation rules of boolean expressions are shown by rules (B1–B6). These rules enable us to obtain the overall value of arithmetic and boolean expressions respectively after solving variables in them. Figure 6 concerns semantic equivalence rules to normalize a program without linear constraints at a state while Fig. 7 lists semantic equivalence rules regarding true and false. In Fig. 8, rules (TR1) and (TR2) deal with interval transition between different states whereas (Nor-Or) and (CONG II) handle transition within a state. Rule (TR1) claims that the current state s i is appended to the model σ i−1, p requests to be executed at the next state s i+1, and the number of states increases by one. Rule (TR2) declares that s i is attached to σ i−1 and the final configuration is reached. (Non-Or) tells us that we can arbitrarily select one subprogram to execute when p 1∨p 2 is encountered in programs. Rule (CONG II) characterizes the replacement of prog with prog′ in configurations as long as prog≡prog′.

Fig. 5
figure 5

Evaluation rules of arithmetic and boolean expressions

Full size image
Fig. 6
figure 6

Semantic equivalence rules

Full size image
Fig. 7
figure 7

Semantic equivalence rules of truth values

Full size image
Fig. 8
figure 8

Interval transition rules and transition rules within a state

Full size image

1.4 Pseudo-code of Simplex algorithm

The pseudo-code of Simplex algorithm is shown in Table 16, which is directly taken from Chap. 29 in Cormen et al. (2005).

Table 16 Simplex algorithm
Full size table

Rights and permissions

Reprints and permissions

About this article

Cite this article

Ma, Q., Duan, Z. Linear time-dependent constraints programming with MSVL. J Comb Optim 27, 724–766 (2014). https://doi.org/10.1007/s10878-012-9551-2

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10878-012-9551-2

Keywords

Search

Navigation