Свойства предикатного трансформера системы VRS
Розглянуто моделі, записані в мові базових протоколів. Вони є атрибутними транзиційними системами, а їх стани задаються формулами багатосортного числення предикатів першого порядку над атрибутами системи. Допускаються атрибути простих числових символьних типів, функціональних типів, а також черги. В...
Saved in:
| Published in: | Кибернетика и системный анализ |
|---|---|
| Date: | 2010 |
| Main Authors: | , , , , |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2010
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/45239 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский, А.А. Летичевский (мл.), С.В. Потиенко, В.С. Песчаненко // Кибернетика и системный анализ. — 2010. — № 4. — С. 3-16. — Бібліогр.: 19 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1862618760076066816 |
|---|---|
| author | Летичевский, А.А. Годлевский, А.Б. Летичевский, А.А. (мл.) Потиенко, С.В. Песчаненко, В.С. |
| author_facet | Летичевский, А.А. Годлевский, А.Б. Летичевский, А.А. (мл.) Потиенко, С.В. Песчаненко, В.С. |
| citation_txt | Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский, А.А. Летичевский (мл.), С.В. Потиенко, В.С. Песчаненко // Кибернетика и системный анализ. — 2010. — № 4. — С. 3-16. — Бібліогр.: 19 назв. — рос. |
| collection | DSpace DC |
| container_title | Кибернетика и системный анализ |
| description | Розглянуто моделі, записані в мові базових протоколів. Вони є атрибутними транзиційними системами, а їх стани задаються формулами багатосортного числення предикатів першого порядку над атрибутами системи. Допускаються атрибути простих числових символьних типів, функціональних типів, а також черги. В постумовах базових протоколів використовуються оператори присвоювання, оновлення черг та довільні формули. Для здійснення переходу із одного стану в інший побудовано предикатний трансформер як функцію перетворення формул. Доведено основну властивість предикатного трансформера, згідно якій він обчислює найсильнішу постумову для символьних станів.
The paper considers models specified in basic protocol language. They are attribute transition systems and their states are defined by formulas of first-order multisort predicate calculus over system attributes. Attributes of simple numeric and symbolic types, functional types, and queues are allowed. Assignment operators, queue update operators, and arbitrary formulas are used in postconditions of basic protocols. To pass from one state to another, a predicate transformer has been set up as a function of formula transformation. The main property of the predicate transformer has been proved: it calculates the strongest postcondition for symbolic states.
|
| first_indexed | 2025-12-07T13:14:25Z |
| format | Article |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-45239 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0023-1274 |
| language | Russian |
| last_indexed | 2025-12-07T13:14:25Z |
| publishDate | 2010 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Летичевский, А.А. Годлевский, А.Б. Летичевский, А.А. (мл.) Потиенко, С.В. Песчаненко, В.С. 2013-06-10T16:10:12Z 2013-06-10T16:10:12Z 2010 Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский, А.А. Летичевский (мл.), С.В. Потиенко, В.С. Песчаненко // Кибернетика и системный анализ. — 2010. — № 4. — С. 3-16. — Бібліогр.: 19 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/45239 519.686.2 Розглянуто моделі, записані в мові базових протоколів. Вони є атрибутними транзиційними системами, а їх стани задаються формулами багатосортного числення предикатів першого порядку над атрибутами системи. Допускаються атрибути простих числових символьних типів, функціональних типів, а також черги. В постумовах базових протоколів використовуються оператори присвоювання, оновлення черг та довільні формули. Для здійснення переходу із одного стану в інший побудовано предикатний трансформер як функцію перетворення формул. Доведено основну властивість предикатного трансформера, згідно якій він обчислює найсильнішу постумову для символьних станів. The paper considers models specified in basic protocol language. They are attribute transition systems and their states are defined by formulas of first-order multisort predicate calculus over system attributes. Attributes of simple numeric and symbolic types, functional types, and queues are allowed. Assignment operators, queue update operators, and arbitrary formulas are used in postconditions of basic protocols. To pass from one state to another, a predicate transformer has been set up as a function of formula transformation. The main property of the predicate transformer has been proved: it calculates the strongest postcondition for symbolic states. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кибернетика Свойства предикатного трансформера системы VRS Властивості предикатного трансформера системи VRS Properties of a predicate transformer of VRS system Article published earlier |
| spellingShingle | Свойства предикатного трансформера системы VRS Летичевский, А.А. Годлевский, А.Б. Летичевский, А.А. (мл.) Потиенко, С.В. Песчаненко, В.С. Кибернетика |
| title | Свойства предикатного трансформера системы VRS |
| title_alt | Властивості предикатного трансформера системи VRS Properties of a predicate transformer of VRS system |
| title_full | Свойства предикатного трансформера системы VRS |
| title_fullStr | Свойства предикатного трансформера системы VRS |
| title_full_unstemmed | Свойства предикатного трансформера системы VRS |
| title_short | Свойства предикатного трансформера системы VRS |
| title_sort | свойства предикатного трансформера системы vrs |
| topic | Кибернетика |
| topic_facet | Кибернетика |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/45239 |
| work_keys_str_mv | AT letičevskiiaa svoistvapredikatnogotransformerasistemyvrs AT godlevskiiab svoistvapredikatnogotransformerasistemyvrs AT letičevskiiaaml svoistvapredikatnogotransformerasistemyvrs AT potienkosv svoistvapredikatnogotransformerasistemyvrs AT pesčanenkovs svoistvapredikatnogotransformerasistemyvrs AT letičevskiiaa vlastivostípredikatnogotransformerasistemivrs AT godlevskiiab vlastivostípredikatnogotransformerasistemivrs AT letičevskiiaaml vlastivostípredikatnogotransformerasistemivrs AT potienkosv vlastivostípredikatnogotransformerasistemivrs AT pesčanenkovs vlastivostípredikatnogotransformerasistemivrs AT letičevskiiaa propertiesofapredicatetransformerofvrssystem AT godlevskiiab propertiesofapredicatetransformerofvrssystem AT letičevskiiaaml propertiesofapredicatetransformerofvrssystem AT potienkosv propertiesofapredicatetransformerofvrssystem AT pesčanenkovs propertiesofapredicatetransformerofvrssystem |