Abstract
In formal verification and system monitoring, the "request-response" pattern is ubiquitous. While conventionally expressed in Linear Temporal Logic (LTL) as $G(req \to F resp)$, this baseline is often too vague for industrial applications. This paper introduces a rigorous six-way classification of request-response specifications, provides a decision tree to help engineers choose the right one, and formalizes these types across grammars, temporal logics, and automata.
Introduction
The standard requirement that "whenever a request happens, a response must eventually follow" serves as a cornerstone of system property specification. However, real-world systems exhibit nuanced requirements regarding redundancy, counting, and unsolicited actions. For instance, if a user inserts two coins into a vending machine, does a single "dispense" action satisfy both requests, or are two required? Can a response occur without a preceding request, such as a waiter checking on a table proactively?
Failing to distinguish between these variations leads to "spec-mining" errors or monitors that flag intended behaviors as bugs. This research fills the gap between abstract logic and practical engineering by providing a structured taxonomy of request-response (req-resp) behaviors.
A Taxonomy of Request-Response Patterns
The authors identify three core criteria to define the behavior of a system's request-response cycle:
- C1 (Multiple Pending): Are multiple pending requests allowed at once?
- C2 (Redundancy): Does one response resolve all currently pending requests?
- C3 (Unsolicited): Are unrequested responses allowed (responses without a matching request)?
By organizing these criteria into a decision tree, the authors derive six distinct types, labeled RR1 through RR6. These types categorize common industrial patterns:
- RR1 (The Waiter): Multiple calls are allowed; one attendance clears all pending calls; unrequested check-ins are permitted.
- RR2 (Network Ack): Multiple sends are allowed; one Ack clears all; however, no Acks are permitted without a prior send.
- RR3 (MQTT Broker): Multiple requests are allowed, but each requires a separate response. Multiple responses per request are possible due to retries.
- RR4 (Vending Machine): Strict 1-to-1 counting; no free items are allowed.
- RR5 (Numbered Tickets): Only one pending request is allowed at a time, though unrequested calls are possible.
- RR6 (Toggle Switch): Strict alternation between "on" and "off" states.
Multi-Formalism Mapping
To ensure these types are usable across different toolchains, the paper provides mathematical definitions for each type in three distinct formats:
Grammars
For simpler, regular types, the authors use regular expressions. For types requiring counting (like RR3 and RR4), they utilize Context-Free Grammars (CFGs). This allows the use of industrial parsers like Menhir or Antlr for system monitoring.
Logic
While standard LTL suffices for regular types, it cannot handle the "counting" requirements of non-regular types. For these, the authors employ CaRet, a temporal logic originally designed for software call stacks, effectively bridging programming language theory and system monitoring.
Automata
The specifications are mapped to standard finite state machines for regular types and Visibly One-Counter Automata (VOCA) for non-regular types. VOCAs use a single integer counter to track the number of pending requests, providing a formal model for properties that require memory of past events.
Key Insights and Results
A critical finding of the research is the distinction between Regular and Non-Regular types. Types RR3 and RR4 are non-regular, meaning a standard finite-state monitor cannot handle them because they require an unbounded counter to track "in-flight" requests.
The authors also highlight the importance of viewpoints. The "correct" specification often depends on the observer; in an MQTT protocol, a broker might observe an RR3 pattern, while an end client might perceive the interaction differently.
Mathematically, the authors prove the equivalence between their CFG definitions and their CaRet logic definitions (Theorems 4.1 and 4.2). In terms of practical monitoring, they demonstrate that while regular types (RR1, 2, 5, 6) are easily monitored with standard logic tools, counting types are currently best handled by repurposing general-purpose parsers, as dedicated one-counter monitors remain rare in the industry.
Limitations and Future Work
The current formalizations assume that a request and a response cannot occur at the exact same timestamp. Lifting this "one-at-a-time" assumption is a primary goal for future research. Additionally, the authors note a tool gap for high-performance "visibly one-counter" property monitors. Finally, while this work focuses on the sequence of events, the integration of real-time constraints (e.g., "response must occur within $n$ seconds") remains a logical next step for the framework.