基于PRISM的自主代理行为建模——一个案例研究
Autonomous Agent Behaviour Modelled in PRISM -- A Case Study
AI总结：
本文提出了一种抽象的自主性定义，用于建模自主场景，并通过小规模仿真模型推断定量数据，以验证无人飞行器在自主场景中的行为。
摘要：
由于自主系统需要被证明安全，对代表机器人行为的代理进行形式验证正成为一个重要领域。本文提出了一种抽象的自主性定义，可用于建模自主场景，并提出使用小规模仿真模型来表示抽象动作以推断定量数据。为了展示该方法的适用性，我们构建并验证了一个无人飞行器（UAV）在示例自主场景中的模型，利用该方法进行验证。
英文摘要：
Formal verification of agents representing robot behaviour is a growing area due to the demand that autonomous systems have to be proven safe. In this paper we present an abstract definition of autonomy which can be used to model autonomous scenarios and propose the use of small-scale simulation models representing abstract actions to infer quantitative data. To demonstrate the applicability of the approach we build and verify a model of an unmanned aerial vehicle (UAV) in an exemplary autonomous scenario, utilising this approach.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
