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
입출력(I/O) 오토마타와 시간적 동작 논리(TLA)는 동시 시스템의 사양 및 검증을 위한 두 가지 잘 알려진 기술입니다. 지난 몇 년 동안 모바일 에이전트 시스템에 더 적합하도록 소위 동적 I/O 오토마타와 각각 모바일 TLA(MTLA)로 확장되었습니다. 동적 I/O 오토마타는 단지 수학적 모델인 반면 MTLA는 공식적으로 정의된 언어를 사용하는 논리입니다. 따라서 본 논문에서는 MTLA가 동적 I/O 오토마타 사양을 위한 공식 언어로 어떻게 사용될 수 있는지 조사합니다. 우리는 해당 모델에 대한 문헌에서 반공식적으로 지정된 여행사 시스템의 MTLA 사양을 작성하여 이를 수행합니다. 이 사양에서는 항상 존재하는 에이전트뿐만 아니라 처음에 알 수 없는 수의 동적으로 생성된 에이전트, 모바일 및 비모바일 에이전트, I/O 자동화 스타일 통신, 모바일 에이전트의 변화하는 통신 기능을 다룹니다. . 우리는 이전에 이 시스템의 TLA 사양을 작성했습니다. 본 논문에서는 이러한 시스템의 MTLA 사양이 TLA와 같은 특수 변수 대신 에이전트 및 위치 이름을 사용하여 에이전트 존재 및 위치를 직접적으로 표현할 수 있기 때문에 동적 I/O 오토마타 정의에 더욱 우아하고 충실할 수 있음을 보여줍니다. 또한 MTLA에서 동적 I/O 오토마타 프레임워크 내에서 동적으로 생성 및 삭제된 에이전트에 대한 이름 재사용을 지정하는 방법도 보여줍니다.
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.
부
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
부
@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},}
부
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 -