nfer

a language and tool for inferring interval abstractions from event traces

This page describes research related to nfer. The nfer tool can be found at http://nfer.io/.

Nfer was developed in collaboration between researchers in Canada and from the NASA Jet Propulsion Laboratory in the USA (Kauffman et al., 2016). It was designed to help operators of the Mars Science Laboratory (Curiosity rover) and other spacecraft better understand these remote systems (Kauffman et al., 2016). Nfer creates abstractions of event streams, meaning the information produced by applying nfer rules is easier to comprehend than directly accessing the event stream. Nfer abstractions form a hierarchy of temporal intervals: they can be built up from smaller pieces to find meaningful information. Applying an nfer specification can also be understood as adding prior knowledge to a trace, transforming it into a more easily analyzed representation (Kauffman et al., 2018). Nfer specifications consisting of only before relations can also be mined from real-time system traces (Kauffman & Fischmeister, 2017).

A :- B before C

A :- B meet C

A :- B during C

A :- B coincide C

A :- B start C

A :- B finish C

A :- B overlap C

A :- B slice C

The eight nfer inclusive operators: before, meet, during, coincide, start, finish, overlap, and slice

Nfer is also a tool that implements the eponymous language(Kauffman, 2021). The tool takes an event stream as an input, such as a program log, and applies a specification to the stream to calculate new information in the form of intervals. In nfer, an interval refers to a piece of data with a label (also called an identifier or name) and two timestamps indicating when it began and ended. Intervals can also carry data, such as integers and strings, in a map. Events in the input are also considered intervals where the begin and end timestamps are identical. An nfer specification consists of rules that each relate (usually) two intervals to one another. When two intervals match, a new interval is produced using information from the rule to determine the label, timestamps, and data (Kauffman, 2023).

Recent work analyzing the evaluation complexity of nfer has shown that it is undecidable for the full language, but with numerous decidable fragments (Kauffman & Zimmermann, 2022). Notably, nfer evaluation under the minimality meta-constraint is in PTime (Kauffman & Zimmermann, 2024). Minimality restricts nfer to produce only intervals that are minimal in their timestamps; they do not contain another interval with the same identifier during the same time period. Nfer satisfiability is also undecidable in the general case, even without data, but a PTime algorithm exists for satisfiability without data and without cycles (Kauffman et al., 2024).

Minimality discards the shaded interval produced by A :- B before C

For humans to use nfer for event trace comprehension, the hierarchy of intervals it produces must be visualized. However, displaying the output of nfer comes with a unique set of challenges because of its hierarchical and concurrent nature. Visualizing these intervals has been the subject of some recent work that has found solutions to the problems inherent when data has duration and hierarchy (Sadman et al., 2025)

Visualization with Nvis

References

2025

Visualizing Temporal Interval Hierarchies

Nafiz Sadman , Nastaran Kian Ersi , and Sean Kauffman

In NASA Formal Methods (NFM’25), Williamsburg, USA, Jun 2025

Abs DOI Bib

We introduce a method for visualizing the temporal intervals output by nfer, a language and tool for event trace comprehension. Visualizing these intervals is challenging because they may be arbitrarily nested in a hierarchy and because multiple intervals with the same identifier may occur concurrently. Our tool, nvis, solves these problems to present the output of nfer in a human interpretable, interactive web interface. We introduce an algorithm to solve the hierarchy and concurrency problem, and present a case study using automatically learned rules from our industrial partner.
@inproceedings{sadman2025visualizing, title = {Visualizing Temporal Interval Hierarchies}, author = {Sadman, Nafiz and Kian Ersi, Nastaran and Kauffman, Sean}, booktitle = {{NASA} Formal Methods {(NFM'25)}}, year = {2025}, month = jun, publisher = {Springer}, series = {LNCS}, volume = {15682}, isbn = {978-3-031-93705-7}, doi = {10.1007/978-3-031-93706-4_19}, location = {Williamsburg, USA}, selected = true, preview = nvis.svg }

2024

The Complexity of Evaluating nfer

Sean Kauffman and Martin Zimmermann

Science of Computer Programming, Jun 2024

Abs DOI Bib

Nfer is a rule-based language for abstracting event streams into a hierarchy of intervals with data. Nfer has multiple implementations and has been applied in the analysis of spacecraft telemetry and autonomous vehicle logs. This work provides the first complexity analysis of nfer evaluation, i.e., the problem of deciding whether a given interval is generated by applying rules. We show that the full nfer language is undecidable and that this depends on both recursion in the rules and an infinite data domain. By restricting either or both of those capabilities, we obtain tight decidability results. We also examine the impact on complexity of exclusive rules and minimality. For the most practical case, which is minimality with finite data, we provide a polynomial-time algorithm.
@article{kauffman2024complexity, title = {The Complexity of Evaluating nfer}, author = {Kauffman, Sean and Zimmermann, Martin}, journal = {Science of Computer Programming}, volume = {231}, year = {2024}, issn = {0167-6423}, doi = {10.1016/j.scico.2023.103012}, selected = true, preview = scp-journal.jpg, keywords = {Interval logic, Complexity, Runtime verification} }
The Complexity of Data-Free Nfer

Sean Kauffman , Kim Guldstrand Larsen , and Martin Zimmermann

In International Conference on Runtime Verification (RV’24), Instanbul, Turkey, Oct 2024

Abs DOI Bib

Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evaluation and satisfiability problems for the data-free fragment of nfer. The evaluation problem asks whether a given interval is generated by applying rules to a known input, while the satisfiability problem asks if an input exists that will generate a given interval. By excluding data from the language, we achieve PTime complexity for the evaluation problem and satisfiability when only considering inclusive rules, and decidability for the satisfiability problem for cycle-free specifications. Finally, we show that for the full data-free language, satisfiability is undecidable.
@inproceedings{kauffman2024datafree, title = {The Complexity of Data-Free Nfer}, author = {Kauffman, Sean and Guldstrand Larsen, Kim and Zimmermann, Martin}, booktitle = {International Conference on Runtime Verification (RV'24)}, publisher = {Springer}, year = {2024}, month = oct, pages = {174--191}, series = {LNCS}, volume = {15191}, isbn = {978-3-031-74233-0}, doi = {10.1007/978-3-031-74234-7_11}, location = {Instanbul, Turkey}, selected = true, preview = rv24-logo.svg }

2023

Log Analysis and System Monitoring with nfer

Sean Kauffman

Science of Computer Programming, Jan 2023

Abs DOI

Nfer is a tool that implements the eponymous language for log analysis and monitoring. Users write rules to calculate new information from an event stream such as a program log either offline or online. In addition to a command-line program, nfer exposes interfaces in Python and R and can generate monitors for embedded systems. Nfer is designed to be fast and has been repeatedly demonstrated to outperform similar tools.

2022

The Complexity of Evaluating nfer

Sean Kauffman and Martin Zimmermann

In International Symposium on Theoretical Aspects of Software Engineering (TASE’22), Jul 2022

Abs DOI

Nfer is a rule-based language for abstracting event streams into a hierarchy of intervals with data. Nfer has multiple implementations and has been applied in the analysis of spacecraft telemetry and autonomous vehicle logs. This work provides the first complexity analysis of nfer evaluation, i.e., the problem of deciding whether a given interval is generated by applying rules. We show that the full nfer language is undecidable and that this depends on both recursion in the rules and an infinite data domain. By restricting either or both of those capabilities, we obtain tight decidability results. We also examine the impact on complexity of exclusive rules and minimality. For the most practical case, which is minimality with finite data, we provide a polynomial time algorithm.

2021

nfer – A Tool for Event Stream Abstraction

Sean Kauffman

In International Conference on Software Engineering and Formal Methods (SEFM’21), Jul 2021

Abs DOI

This work describes nfer, an open-source tool for event-stream abstraction and processing. Nfer implements the Runtime Verification logic of the same name, providing programming interfaces in C, R, and Python. Rules that dictate nfer’s behavior can be written in an external Domain-Specific Language (DSL), mined from historical traces, or given using an internal DSL in Python. The tool is designed for efficient online monitoring of event streams and can also operate as an offline tool to process completed logs.

2018

Inferring Event Stream Abstractions

Sean Kauffman , Klaus Havelund , Rajeev Joshi , and Sebastian Fischmeister

Formal Methods in System Design, Jul 2018

Abs DOI

We propose a formalism for specifying event stream abstractions for use in spacecraft telemetry processing. Our work is motivated by the need to quickly process streams with millions of events generated by the Curiosity rover on Mars. The approach builds a hierarchy of event abstractions for telemetry visualization and querying to aid human comprehension. Such abstractions can also be used as input to other runtime verification tools. Our notation is inspired by Allen’s Temporal Logic, and provides a rule-based declarative way to express event abstractions. We present an algorithm for applying specifications to an event stream and explore modifications to improve the algorithm’s asymptotic complexity. The system is implemented in both Scala and C, with the specification language implemented as internal as well as external DSLs. We illustrate the solution with several examples, a performance evaluation, and a real telemetry analysis scenario.

2017

Mining Temporal Intervals from Real-time System Traces

Sean Kauffman and Sebastian Fischmeister

In International Workshop on Software Mining (SoftwareMining’17), Jul 2017

Abs DOI

We introduce a novel algorithm for mining temporal intervals from real-time system traces with linear complexity using passive, black-box learning. Our interest is in mining nfer specifications from spacecraft telemetry to improve human and machine comprehension. Nfer is a recently proposed formalism for inferring event stream abstractions with a rule notation based on Allen Logic. The problem of mining Allen’s relations from a multivariate interval series is well studied, but little attention has been paid to generating such a series from symbolic time sequences such as system traces. We propose a method to automatically generate an interval series from real-time system traces so that they may be used as inputs to existing algorithms to mine nfer rules. Our algorithm has linear runtime and constant space complexity in the length of the trace and can mine infrequent intervals of arbitrary length from incomplete traces. The paper includes results from case studies using logs from the Curiosity rover on Mars and two other realistic datasets.

2016

nfer–A Notation and System for Inferring Event Stream Abstractions

Sean Kauffman , Klaus Havelund , and Rajeev Joshi

In International Conference on Runtime Verification (RV’16), Jul 2016

Abs DOI

We propose a notation for specifying event stream abstractions for use in spacecraft telemetry processing. Our work is motivated by the need to quickly process streams with millions of events generated by the Curiosity rover on Mars. The approach builds a hierarchy of event abstractions for telemetry visualization and querying to aid human comprehension. Such abstractions can also be used as input to other runtime verification tools. Our notation is inspired by Allen’s Temporal Logic, and provides a rule-based declarative way to express event abstractions. The system is written in Scala, with the specification language implemented as an internal DSL. It is based on parallel executing actors communicating via a publish-subscribe model. We illustrate the solution with several examples, including a real telemetry analysis scenario.
Towards a logic for inferring properties of event streams

Sean Kauffman , Rajeev Joshi , and Klaus Havelund

In International Symposium on Leveraging Applications of Formal Methods (ISoLA’16), Jul 2016

Abs DOI

We outline the background, motivation, and requirements of an approach to create abstractions of event streams, which are time-tagged sequences of events generated by an executing software system. Our work is motivated by the need to process event streams with millions of events that are generated by a spacecraft, that must be processed quickly after they are received on the ground. Our approach involves building a tool that adds hierarchical labels to a received event stream. The labels add contextual information to the event stream, and thus make it easier to build tools for visualizing and analyzing telemetry. We describe a notation for writing hierarchical labeling rules; the notation is based on a modification of Allen Temporal Logic, augmented with rule-definitions and features for referring to data in data parameterized events. We illustrate our notation and its use with an example.