Свойства предикатного трансформера системы VRS
Розглянуто моделі, записані в мові базових протоколів. Вони є атрибутними транзиційними системами, а їх стани задаються формулами багатосортного числення предикатів першого порядку над атрибутами системи. Допускаються атрибути простих числових символьних типів, функціональних типів, а також черги. В...
Збережено в:
| Опубліковано в: : | Кибернетика и системный анализ |
|---|---|
| Дата: | 2010 |
| Автори: | , , , , |
| Формат: | Стаття |
| Мова: | Russian |
| Опубліковано: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2010
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/45239 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский, А.А. Летичевский (мл.), С.В. Потиенко, В.С. Песчаненко // Кибернетика и системный анализ. — 2010. — № 4. — С. 3-16. — Бібліогр.: 19 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-45239 |
|---|---|
| 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 |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Свойства предикатного трансформера системы VRS |
| spellingShingle |
Свойства предикатного трансформера системы VRS Летичевский, А.А. Годлевский, А.Б. Летичевский, А.А. (мл.) Потиенко, С.В. Песчаненко, В.С. Кибернетика |
| title_short |
Свойства предикатного трансформера системы VRS |
| title_full |
Свойства предикатного трансформера системы VRS |
| title_fullStr |
Свойства предикатного трансформера системы VRS |
| title_full_unstemmed |
Свойства предикатного трансформера системы VRS |
| title_sort |
свойства предикатного трансформера системы vrs |
| author |
Летичевский, А.А. Годлевский, А.Б. Летичевский, А.А. (мл.) Потиенко, С.В. Песчаненко, В.С. |
| author_facet |
Летичевский, А.А. Годлевский, А.Б. Летичевский, А.А. (мл.) Потиенко, С.В. Песчаненко, В.С. |
| topic |
Кибернетика |
| topic_facet |
Кибернетика |
| publishDate |
2010 |
| language |
Russian |
| container_title |
Кибернетика и системный анализ |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| format |
Article |
| title_alt |
Властивості предикатного трансформера системи VRS Properties of a predicate transformer of VRS system |
| 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.
|
| issn |
0023-1274 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/45239 |
| citation_txt |
Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский, А.А. Летичевский (мл.), С.В. Потиенко, В.С. Песчаненко // Кибернетика и системный анализ. — 2010. — № 4. — С. 3-16. — Бібліогр.: 19 назв. — рос. |
| 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 |
| first_indexed |
2025-12-07T13:14:25Z |
| last_indexed |
2025-12-07T13:14:25Z |
| _version_ |
1850855407878144000 |