The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Automata Input/Output (I/O) dan Temporal Logic of Actions (TLA) ialah dua teknik yang terkenal untuk spesifikasi dan pengesahan sistem serentak. Sejak beberapa tahun kebelakangan ini, mereka telah diperluaskan kepada apa yang dipanggil automata I/O dinamik dan, masing-masing, Mobile TLA (MTLA) agar lebih sesuai untuk sistem ejen mudah alih. Automata I/O dinamik hanyalah model matematik, manakala MTLA ialah logik dengan bahasa yang ditakrifkan secara formal. Oleh itu, dalam makalah ini, kami menyiasat bagaimana MTLA boleh digunakan sebagai bahasa formal untuk spesifikasi automata I/O dinamik. Kami melakukan ini dengan menulis spesifikasi MTLA bagi sistem ejen pelancongan yang telah dinyatakan secara separuh formal dalam literatur tentang model tersebut. Dalam spesifikasi ini, kami berurusan dengan ejen yang sentiasa sedia ada serta dengan bilangan ejen yang dicipta secara dinamik yang pada mulanya tidak diketahui, dengan ejen mudah alih dan bukan mudah alih, dengan komunikasi gaya I/O-automata, dan dengan keupayaan komunikasi yang berubah-ubah ejen mudah alih. . Kami sebelum ini telah menulis spesifikasi TLA sistem ini. Kertas kerja ini menunjukkan bahawa spesifikasi MTLA bagi sistem sedemikian boleh menjadi lebih elegan dan setia kepada definisi automata I/O dinamik kerana kewujudan dan lokasi ejen boleh dinyatakan secara langsung dengan menggunakan nama ejen dan lokasi dan bukannya pembolehubah khas seperti dalam TLA. Ia juga menunjukkan cara penggunaan semula nama untuk ejen yang dicipta dan dimusnahkan secara dinamik dalam rangka kerja automata I/O dinamik boleh ditentukan dalam MTLA.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Salinan
Tatjana KAPUS, "Using Mobile TLA as a Logic for Dynamic I/O Automata" in IEICE TRANSACTIONS on Information,
vol. E92-D, no. 8, pp. 1515-1522, August 2009, doi: 10.1587/transinf.E92.D.1515.
Abstract: Input/Output (I/O) automata and the Temporal Logic of Actions (TLA) are two well-known techniques for the specification and verification of concurrent systems. Over the past few years, they have been extended to the so-called dynamic I/O automata and, respectively, Mobile TLA (MTLA) in order to be more appropriate for mobile agent systems. Dynamic I/O automata is just a mathematical model, whereas MTLA is a logic with a formally defined language. In this paper, therefore, we investigate how MTLA could be used as a formal language for the specification of dynamic I/O automata. We do this by writing an MTLA specification of a travel agent system which has been specified semi-formally in the literature on that model. In this specification, we deal with always existing agents as well as with an initially unknown number of dynamically created agents, with mobile and non-mobile agents, with I/O-automata-style communication, and with the changing communication capabilities of mobile agents. We have previously written a TLA specification of this system. This paper shows that an MTLA specification of such a system can be more elegant and faithful to the dynamic I/O automata definition because the agent existence and location can be expressed directly by using agent and location names instead of special variables as in TLA. It also shows how the reuse of names for dynamically created and destroyed agents within the dynamic I/O automata framework can be specified in MTLA.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E92.D.1515/_p
Salinan
@ARTICLE{e92-d_8_1515,
author={Tatjana KAPUS, },
journal={IEICE TRANSACTIONS on Information},
title={Using Mobile TLA as a Logic for Dynamic I/O Automata},
year={2009},
volume={E92-D},
number={8},
pages={1515-1522},
abstract={Input/Output (I/O) automata and the Temporal Logic of Actions (TLA) are two well-known techniques for the specification and verification of concurrent systems. Over the past few years, they have been extended to the so-called dynamic I/O automata and, respectively, Mobile TLA (MTLA) in order to be more appropriate for mobile agent systems. Dynamic I/O automata is just a mathematical model, whereas MTLA is a logic with a formally defined language. In this paper, therefore, we investigate how MTLA could be used as a formal language for the specification of dynamic I/O automata. We do this by writing an MTLA specification of a travel agent system which has been specified semi-formally in the literature on that model. In this specification, we deal with always existing agents as well as with an initially unknown number of dynamically created agents, with mobile and non-mobile agents, with I/O-automata-style communication, and with the changing communication capabilities of mobile agents. We have previously written a TLA specification of this system. This paper shows that an MTLA specification of such a system can be more elegant and faithful to the dynamic I/O automata definition because the agent existence and location can be expressed directly by using agent and location names instead of special variables as in TLA. It also shows how the reuse of names for dynamically created and destroyed agents within the dynamic I/O automata framework can be specified in MTLA.},
keywords={},
doi={10.1587/transinf.E92.D.1515},
ISSN={1745-1361},
month={August},}
Salinan
TY - JOUR
TI - Using Mobile TLA as a Logic for Dynamic I/O Automata
T2 - IEICE TRANSACTIONS on Information
SP - 1515
EP - 1522
AU - Tatjana KAPUS
PY - 2009
DO - 10.1587/transinf.E92.D.1515
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E92-D
IS - 8
JA - IEICE TRANSACTIONS on Information
Y1 - August 2009
AB - Input/Output (I/O) automata and the Temporal Logic of Actions (TLA) are two well-known techniques for the specification and verification of concurrent systems. Over the past few years, they have been extended to the so-called dynamic I/O automata and, respectively, Mobile TLA (MTLA) in order to be more appropriate for mobile agent systems. Dynamic I/O automata is just a mathematical model, whereas MTLA is a logic with a formally defined language. In this paper, therefore, we investigate how MTLA could be used as a formal language for the specification of dynamic I/O automata. We do this by writing an MTLA specification of a travel agent system which has been specified semi-formally in the literature on that model. In this specification, we deal with always existing agents as well as with an initially unknown number of dynamically created agents, with mobile and non-mobile agents, with I/O-automata-style communication, and with the changing communication capabilities of mobile agents. We have previously written a TLA specification of this system. This paper shows that an MTLA specification of such a system can be more elegant and faithful to the dynamic I/O automata definition because the agent existence and location can be expressed directly by using agent and location names instead of special variables as in TLA. It also shows how the reuse of names for dynamically created and destroyed agents within the dynamic I/O automata framework can be specified in MTLA.
ER -