Devising a strategy to make a system mimicking behaviors from another system
is a problem that naturally arises in many areas of Computer Science. In this
work, we interpret this problem in the context of intelligent agents, from the
perspective of LTLf, a formalism commonly used in AI for expressing
finite-trace properties. Our model consists of two separated dynamic domains,
D_A and D_B, and an LTLf specification that formalizes the notion of mimicking
by mapping properties on behaviors (traces) of D_A into properties on behaviors
of D_B. The goal is to synthesize a strategy that step-by-step maps every
behavior of D_A into a behavior of D_B so that the specification is met. We
consider several forms of mapping specifications, ranging from simple ones to
full LTLf, and for each we study synthesis algorithms and computational
properties.

本文介绍了基于智能代理的 LTLf 形式化方法来解决计算机科学中的系统模仿问题，从简单映射到全 LTLf 并研究了合成算法和计算性质。

分离领域中的行为模仿

Mimicking Behaviors in Separated Domains

Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a
de-facto standard to produce specifications in many application domains (e.g.,
planning, business process management, run-time monitoring, reactive
synthesis). Several studies approached the respective satisfiability problem.
In this paper, we investigate the problem of extracting the unsatisfiable core
in LTLf specifications. We provide four algorithms for extracting an
unsatisfiable core leveraging the adaptation of state-of-the-art approaches to
LTLf satisfiability checking. We implement the different approaches within the
respective tools and carry out an experimental evaluation on a set of reference
benchmarks, restricting to the unsatisfiable ones. The results show the
feasibility, effectiveness, and complementarities of the different algorithms
and tools.

本文提出四种算法用于提取 LTLf 规范中的不可满足核，并采用实验评估了各种算法和工具的可行性、有效性和互补性。