000 02590n a2200325#a 4500
001 21719
003 P5A
005 20221213140139.0
008 950209s1994 dk a tb 000 0 eng d
035 _aocm31960448
040 _aPMC
_cPMC
049 _aP5AA
090 _atext
100 1 _aJensen, Ole H.
_923128
245 1 0 _aModel construction for hybrid implicit specifications/
_cby Ole Hogh Jensen, Christian Jeppesen, Jarl Tuxen Lang.
260 _aAalborg, Denmark:
_bUniversity of Aalborg, Institute for Electronic Systems, Dept. of Mathematics and Computer Science,
_c[1994].
300 _aviii, 150 p.:
_bill.;
_c24 cm.
490 1 _aReport / University of Aalborg. Institute for Electronic Systems. Dept. of Mathematics and Computer Science,;
_x0106-0791;
_vR 94-2012
500 _aCover title.
500 _a"March 1994."
502 _aThesis (M.S.)--Aalborg University, 1994.
504 _aIncludes bibliographical references.
520 _aAbstract: "Top-down design of a reactive system, such as a computer program, can be viewed as a stepwise refinement of a specification. In order to ensure that the specification is indeed a correct description of the desired system, it is advantageous to be able to synthesize (perhaps automatically) prototypes from specifications. This thesis considers model construction, i.e. synthesis of prototypes, for hybrid implicit specifications of the form C(P₁ ..., P[subscript n];G₁ ..., G[subscript m]) sat F asserting that the process C(P₁ ..., P[subscript n];Q₁ ..., Q[subscript m]) satisfies the specification F whenever the process Q[subscript i] satisfies the specification G[subscript i] for 1 [<or =] i [<or =] m. We offer the theoretical development of a tableau-like method for constructing the processes P₁ ..., P[subscript n] (as labelled transition systems) when C is given as a context of process algebra (such as CCS), and F is given as a formula of Hennessy-Milner Logic with maximal recursion. Furthermore, we report on a prototype implementation of a model construction tool based on the presented theory."
650 0 4 _aComputer programs.
_937456
697 _aTeses Externas
_924308
700 1 _aJeppesen, Christian
_923129
700 1 _aLang, Jarl Tuxen
_923130
830 0 _aReport (Aalborg universitetscenter. Afdeling for matematik og datalogi);
_vR 94-2012.
_929882
942 _2impa
_cTHESIS
999 _aJENSEN, Ole H.; JEPPESEN, Christian; LANG, Jarl Tuxen. <b> Model construction for hybrid implicit specifications. </b> Aalborg, Denmark, [1994]. viii, 150 p. Thesis (M.S.)--Aalborg University, 1994.
_c21951
_d21951