Bensalem, SaddekSaddekBensalemCheng, Chih-HongChih-HongChengHuang, XiaoweiXiaoweiHuangKatsaros, PanagiotisPanagiotisKatsarosMolin, AdamAdamMolinNickovic, DejanDejanNickovicPeled, DoronDoronPeled2023-01-022023-01-022022https://publica.fraunhofer.de/handle/publica/43044410.1007/978-3-031-21222-2_8The formal specification provides a uniquely readable description of various aspects of a system, including its temporal behavior. This facilitates testing and sometimes automatic verification of the system against the given specification. We present a logic-based formalism for specifying learning-enabled autonomous systems, which involve components based on neural networks. The formalism is based on first-order past time temporal logic that uses predicates for denoting events. We have applied the formalism successfully to two complex use cases.enautonomous systemslearning-enabled systemsformal specificationneural networksfirst-order LTLconference paper