In this paper, it is shown that stable model semantics, perfect model semantics, and partial stable model semantics of disjunctive logic programs have the same expressive power with respect to the polynomial-time mode...In this paper, it is shown that stable model semantics, perfect model semantics, and partial stable model semantics of disjunctive logic programs have the same expressive power with respect to the polynomial-time model-equivalent reduction. That is, taking perfect model semantics and stable model semantic as an example, any logic program P can be transformed in polynomial time to another logic program P＇ such that perfect models （resp. stable models） of P i-i correspond to stable models （resp. perfect models） of P＇, and the correspondence can be computed also in polynomial time. However, the minimal model semantics has weaker expressiveness than other mentioned semantics, otherwise, the polynomial hierarchy would collapse to NP.展开更多
SIGNAL is a part of the synchronous languages family, which are broadly used in the design of safety-critical real-time systems such as avionics, space systems, and nu- clear power plants. There exist several semantic...SIGNAL is a part of the synchronous languages family, which are broadly used in the design of safety-critical real-time systems such as avionics, space systems, and nu- clear power plants. There exist several semantics for SIG- NAL, such as denotational semantics based on traces （called trace semantics）, denotational semantics based on tags （called tagged model semantics）, operational semantics presented by structural style through an inductive definition of the set of possible transitions, operational semantics defined by syn- chronous transition systems （STS）, etc. However, there is lit- tle research about the equivalence between these semantics. In this work, we would like to prove the equivalence be- tween the trace semantics and the tagged model semantics, to get a determined and precise semantics of the SIGNAL language. These two semantics have several different defini- tions respectively, we select appropriate ones and mechanize them in the Coq platform, the Coq expressions of the abstract syntax of SIGNAL and the two semantics domains, i.e., the trace model and the tagged model, are also given. The dis- tance between these two semantics discourages a direct proof of equivalence. Instead, we transform them to an intermediate model, which mixes the features of both the trace semantics and the tagged model semantics. Finally, we get a determined and precise semantics of SIGNAL.展开更多
基金This research was partially supported by the National Natural Science Foundation of China under Grant Nos.60573011,10410638an MOE Project of Key Institute at Universities under Grant No.05JJD72040122.
文摘In this paper, it is shown that stable model semantics, perfect model semantics, and partial stable model semantics of disjunctive logic programs have the same expressive power with respect to the polynomial-time model-equivalent reduction. That is, taking perfect model semantics and stable model semantic as an example, any logic program P can be transformed in polynomial time to another logic program P＇ such that perfect models （resp. stable models） of P i-i correspond to stable models （resp. perfect models） of P＇, and the correspondence can be computed also in polynomial time. However, the minimal model semantics has weaker expressiveness than other mentioned semantics, otherwise, the polynomial hierarchy would collapse to NP.
文摘SIGNAL is a part of the synchronous languages family, which are broadly used in the design of safety-critical real-time systems such as avionics, space systems, and nu- clear power plants. There exist several semantics for SIG- NAL, such as denotational semantics based on traces （called trace semantics）, denotational semantics based on tags （called tagged model semantics）, operational semantics presented by structural style through an inductive definition of the set of possible transitions, operational semantics defined by syn- chronous transition systems （STS）, etc. However, there is lit- tle research about the equivalence between these semantics. In this work, we would like to prove the equivalence be- tween the trace semantics and the tagged model semantics, to get a determined and precise semantics of the SIGNAL language. These two semantics have several different defini- tions respectively, we select appropriate ones and mechanize them in the Coq platform, the Coq expressions of the abstract syntax of SIGNAL and the two semantics domains, i.e., the trace model and the tagged model, are also given. The dis- tance between these two semantics discourages a direct proof of equivalence. Instead, we transform them to an intermediate model, which mixes the features of both the trace semantics and the tagged model semantics. Finally, we get a determined and precise semantics of SIGNAL.
