Methods of forward and backward symbolic modeling of systems specified by basic protocols
The paper considers methods of forward and backward symbolic modeling which are used for solution of verification tasks for basic protocols systems. Besides of algorithms for state space search detailed in model checking works, the main task of symbolic modeling is implementation of transition from...
Saved in:
| Date: | 2026 |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
PROBLEMS IN PROGRAMMING
2026
|
| Subjects: | |
| Online Access: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/1014 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Problems in programming |
| Download file: |  |
Institution
Problems in programming| Summary: | The paper considers methods of forward and backward symbolic modeling which are used for solution of verification tasks for basic protocols systems. Besides of algorithms for state space search detailed in model checking works, the main task of symbolic modeling is implementation of transition from one state class to the next. Such a transformation is realized by predicate transformers. In the current work, algorithms of forward and backward predicate transformers have been built for numeric, symbolic, and lists data structures. Transformers are considered as functions which derive from given formula a new one that defines state class of the system after transition made by given basic protocol.Problems in programming 2008; 4: 39-44 |
|---|