Predicate transformers in the context of symbolic modeling of transition systems

被引:0
|
作者
A. B. Godlevsky
机构
[1] National Academy of Sciences of Ukraine,Cybernetics Institute
关键词
attribute transition systems; symbolic modeling; predicate transformer; basic protocol;
D O I
10.1007/s10559-010-9236-8
中图分类号
学科分类号
摘要
In modelling attribute transition systems, classes of their states can be described in a given signature of functional and predicate symbols. A procedure is developed for transforming such formulas by assignment operators and the obtained formulas are proved to correspond to strongest postconditions. A peculiarity of this paper is that functional-type attributes can be used in specifying transition systems, in particular, their array-type attributes.
引用
收藏
页码:602 / 608
页数:6
相关论文
共 50 条