Author name cluster

K. Narayan Kumar

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

2 author rows

TCS Journal 2015 Journal Article

Checking conformance for time-constrained scenario-based specifications

S. Akshay
Paul Gastin
Madhavan Mukund
K. Narayan Kumar

We consider the problem of model checking message-passing systems with real-time requirements. As behavioral specifications, we use message sequence charts (MSCs) annotated with timing constraints. Our system model is a network of communicating finite state machines with local clocks, whose global behavior can be regarded as a timed automaton. Our goal is to verify that all timed behaviors exhibited by the system conform to the timing constraints imposed by the specification. In general, this corresponds to checking inclusion for timed languages, which is an undecidable problem even for timed regular languages. However, we show that we can translate regular collections of time-constrained MSCs into a special class of event-clock automata that can be determinized and complemented, thus permitting an algorithmic solution to the model checking/conformance problem.

Details DOI

I&C Journal 2005 Journal Article

A theory of regular MSC languages

Jesper G. Henriksen
Madhavan Mukund
K. Narayan Kumar
Milind Sohoni
P.S. Thiagarajan

Message sequence charts (MSCs) are an attractive visual formalism widely used to capture system requirements during the early design stages in domains such as telecommunication software. It is fruitful to have mechanisms for specifying and reasoning about collections of MSCs so that errors can be detected even at the requirements level. We propose, accordingly, a notion of regularity for collections of MSCs and explore its basic properties. In particular, we provide an automata-theoretic characterization of regular MSC languages in terms of finite-state distributed automata called bounded message-passing automata. These automata consist of a set of sequential processes that communicate with each other by sending and receiving messages over bounded FIFO channels. We also provide a logical characterization in terms of a natural monadic second-order logic interpreted over MSCs. A commonly used technique to generate a collection of MSCs is to use a hierarchical message sequence chart (HMSC). We show that the class of languages arising from the so-called bounded HMSCs constitute a proper subclass of the class of regular MSC languages. In fact, we characterize the bounded HMSC languages as the subclass of regular MSC languages that are finitely generated.

Details DOI

TCS Journal 2003 Journal Article

Bounded time-stamping in message-passing systems

Madhavan Mukund
K. Narayan Kumar
Milind Sohoni

Consider a distributed system running a protocol in which processes exchange information by passing messages. The gossip problem for the protocol is the following: Whenever a process q receives a message from another process p, q must be able to decide which of p and q has more recent information about r, for every other process r in the system. With this data, q is in a position to update its knowledge about the global state of the system. We propose a solution wherein to each message of the protocol, the sender adds information about its current state of knowledge about other processes. We do not add any new messages to the underlying computation. The additional information tagged onto each message is uniformly bounded if the channels are bounded. This means that for systems with bounded channels, the overhead of maintaining the latest gossip is a constant, independent of the length of the underlying computation. Moreover, gossip information can be used to implement bounded channels by inhibiting the sending of new messages over channels that are potentially full. Our solution to the gossip problem has several applications in the analysis of distributed systems. Many distributed algorithms rely, either explicitly or implicitly, on the local information available at a process about the global state of the system. Using our scheme, each process can ensure that during a computation it always maintains the best possible information about every other process. At a theoretical level, the gossip problem plays an important role in formal characterizations of finite-state message-passing systems.

Details DOI

MFCS Conference 2003 Conference Paper

Local LTL with Past Constants Is Expressively Complete for Mazurkiewicz Traces

Paul Gastin
Madhavan Mukund
K. Narayan Kumar

Abstract To obtain an expressively complete linear-time temporal logic (LTL) over Mazurkiewicz traces that is computationally tractable, we need to intepret formulas locally, at individual events in a trace, rather than globally, at configurations. Such local logics necessarily require past modalities, in contrast to the classical setting of LTL over sequences. Earlier attempts at defining expressively complete local logics have used very general past modalities as well as filters (side-conditions) that “look sideways” and talk of concurrent events. In this paper, we show that it is possible to use unfiltered future modalities in conjunction with past constants and still obtain a logic that is expressively complete over traces.

Details

MFCS Conference 2000 Conference Paper

Regular Collections of Message Sequence Charts

Jesper G. Henriksen
Madhavan Mukund
K. Narayan Kumar
P. S. Thiagarajan

Abstract Message Sequence Charts (MSCs) are an attractive visual formalism used during the early stages of design in domains such as telecommunication software. A popular mechanism for generating a collection of MSCs is a Hierarchical Message Sequence Chart (HMSC). However, not all HMSCs describe collections of MSCs that can be “realized” as a finite-state device. Our main goal is to pin down this notion of realizability. We propose an independent notion of regularity for collections of MSCs and explore its basic properties. In particular, we characterize regular collections of MSCs in terms of finite-state distributed automata called bounded message-passing automata, in which a set of sequential processes communicate with each other asynchronously over bounded FIFO channels. We also provide a logical characterization in terms of a natural monadic second-order logic interpreted over MSCs. It turns out that realizable collections of MSCs as specified by HMSCs constitute a strict subclass of the regular collections of MSCs.

Details