Name
Abstract | ||
|---|---|---|
We give an algebraic model of (H3) designs based on a vari- ant of modal semirings, hence generalising the original relational model. This makes the theory applicable to a wider class of settings, e.g., to alge- bras of sets of traces. Moreover, we set up the connection with the weakly and strongly demonic semantics of programs as discussed by a number of authors. This is done using commands (a,t) where a corresponds to the transition relation of a program and the condition t characterises the input states from which termination is guaranteed. The commands form not only a semiring but even a Kleene and omega algebra. This is used to calculate closed expressions for the least and greatest fixed point semantics of the demonic while loop. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11768173_14 | Unifying Theories of Programming |
Keywords | Field | DocType |
algebraic principle,formal connection,modal design algebra,omega algebra,semiring,original relational model,fixpoint,previous algebraic approach,general property,left semiring,kleene algebra,standard utp theory,greatest fixed-point semantics,deeper insight,algebraic model,utp,linear recursion,relational model,fixed point | Galois connection,Kleene algebra,Algebraic number,Expression (mathematics),Algebra,Computer science,Correctness,Algorithm,While loop,Boolean algebra,Semiring | Conference |
Volume | ISSN | ISBN |
4010 | 0302-9743 | 3-540-34750-X |
Citations | PageRank | References |
14 | 0.69 | 27 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Walter Guttmann | 1 | 196 | 16.53 |
| Bernhard Möller | 2 | 788 | 55.89 |