Generic verification of security protocols (2009)
Abdul Sahid Khan, Madhavan Mukund, S. P. Suresh
Abstract. Security protocols are notoriously difficult to debug. One approach to the automatic verification of security protocols with a bounded set of agents uses logic programming with analysis and...
Checking consistency of SDL+MSC specifications? (2008)
Abstract. We consider the problem of checking whether a distributed system described in SDL is consistent with a set of MSCs that constrain the interaction between the processes. In general, the MSC...
Puneet Bhateja, Paul Gastin, Madhavan Mukund, K. Narayan Kumar
testing of message sequence charts
Checking Coverage for Infinite Collections of Timed Scenarios ⋆ (2008)
S. Akshay, Madhavan Mukund, K. Narayan Kumar
Abstract. We consider message sequence charts enriched with timing constraints between pairs of events. As in the untimed setting, an infinite family of time-constrained message sequence charts...
Puneet Bhateja, Paul Gastin, Madhavan Mukund
fresh look at testing for asynchronous
Matching scenarios with timing constraints ⋆ (2008)
Abstract. Networks of communicating finite-state machines equipped with local clocks generate timed MSCs. We consider the problem of checking whether these timed MSCs are “consistent ” with those...
Puneet Bhateja, Paul Gastin, Madhavan Mukund, K. Narayan Kumar
Abstract. Message sequence charts are an attractive formalism for specifying communicating systems. One way to test such a system is to substitute a component by a test process and observe its...
A fresh look at testing for asynchronous communication ⋆ (2008)
Puneet Bhateja, Paul Gastin, Madhavan Mukund
Abstract. Testing is one of the fundamental techniques for verifying if a computing system conforms to its specification. We take a fresh look at the theory of testing for message-passing systems...
Hariharan, Ramesh, Mukund, Madhavan, Vinay, V
This volume contains the proceedings of the 28th international conference on the Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008), organized under the auspices of the...
Hariharan, Ramesh, Mukund, Madhavan, Vinay, V
This volume contains the proceedings of the 28th international conference on the Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008), organized under the auspices of the...
Kamal Lodaya, Madhavan Mukund, R. Ramanujam, P. S. Thiagarajan
A distributed computer system consists of dierent processes or agents that function largely autonomously and coordinate their actions by communicating with each other. In such a situation, actions...
Checking consistency of SDL+MSC specifications ⋆ (2007)
Abstract. We consider the problem of checking whether a distributed system described in SDL is consistent with a set of MSCs that constrain the interaction between the processes. In general, the MSC...
Ilaria Castellani, Madhavan Mukund, P S Thiagarajan
distributed transition systems from global specifications
Finite-state Automata on Infinite Inputs (2007)
This paper is a self-contained introduction to the theory of finite-state automata on infinite words. The study of automata on infinite inputs was initiated by Buchi in order to settle certain...
Generic verification of security protocols (2005)
Abdul Sahid Khan, Madhavan Mukund, S. P. Suresh
Security protocols are notoriously difficult to debug. One approach to the automatic verification of security protocols with a bounded set of agents uses logic programming with analysis and synthesis...
Causal closure for MSC languages (2005)
Bharat Adsul, Madhavan Mukund, K. Narayan Kumar
Abstract. Message sequence charts (MSCs) are commonly used to specify interactions between agents in communicating systems. Their visual nature makes them attractive for describing scenarios, but...
Formal Methods Update Meeting ’05, IIT Bombay, 20 July 2005 – p.3 (2005)
Madhavan Mukund, An Atm, An Atm, An Atm
Messages sent between communicating agents
Generic verification of security protocols (2005)
Abdul Sahid Khan, Madhavan Mukund, S. P. Suresh
Abstract. Security protocols are notoriously difficult to debug. One approach to the automatic verification of security protocols with a bounded set of agents uses logic programming with analysis and...
Relational structures and FOL (2004)
Madhavan Mukund, Ra K, Ra K, ...
� A is the domain—assume countable � Each R A i is a relation on A, with arity ni
Local LTL with past constants is expressively complete for Mazurkiewicz traces (2003)
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...
Netcharts: Bridging the gap between HMSCs and executable specifications (2003)
Madhavan Mukund, K. Narayan Kumar, P. S. Thiagarajan
Abstract. We define a new notation called netcharts for describing sets of message sequence chart scenarios (MSCs). Netcharts correspond to a distributed version of High-level Message Sequence Charts...
A Theory of Regular MSC Languages (2003)
Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, Milind Sohoni, P.S. Thiagaranjan
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...
Bounded time-stamping in message-passing systems (2003)
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...
Hereditary history preserving bisimulation is decidable for trace-labelled systems (2002)
Abstract. Hereditary history preserving bisimulation is a natural extension of bisimulation to the setting of so-called “true ” concurrency. Somewhat surprisingly, this extension turns out to be...
Local and symbolic bisimulation using tabled constraint logic programming (2001)
Samik Basu, Madhavan Mukund, Rakesh Verma
3 1
Local and symbolic bisimulation using tabled constraint logic programming (2001)
Samik Basu, Madhavan Mukund, C. R. Ramakrishnan, I. V. Ramakrishnan, Rakesh Verma
Bisimulation is a fundamental notion that characterizes behavioral equivalence of concurrent systems. In this paper, we study the problem of encoding ecient bisimulation checkers for nite- as well as...
Regular collections of Message Sequence Charts (2000)
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...
Regular Collections of Message Sequence Charts (2000)
Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, P. S. Thiagarajan
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...
Symbolic Bisimulation using Tabled Constraint Logic Programming (2000)
Madhavan Mukund, C. R. Ramakrishnan, I.V. Ramakrishnan, Rakesh Verma
A tabled logic programming system offrs an attractive platform for encoding computational problems in the specification and verification of systems. Model checking, an automatic technique for...
On message sequence graphs and finitely generated regular MSC languages (2000)
Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar
Abstract. 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. A...
A theory of regular MSC languages (1999)
K. Narayan Kumar, P. S. Thiagarajan, Madhavan Mukund, Madhavan Mukund, Jesper G. Henriksen, Jesper G. Henriksen, ...
et al.:
This document in subdirectoryRS/99/52/ Towards a Theory of Regular MSC Languages (1999)
Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, P. S. Thiagarajan, Copyright C, Jesper G. Henriksen, ...
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...
Linear-Time Temporal Logic and Büchi Automata (1997)
Over the past two decades, temporal logic has become a very basic tool for specifying properties of reactive systems. For finite-state systems, it is possible to use techniques based on Buchi...
Keeping Track of the Latest Gossip in a Distributed System (1997)
Madhavan Mukund, Milind Sohoni
We tackle a natural problem from distributed computing, involving time-stamps. Let P = fp 1 ; p 2 ; : : : ; p N g be a set of computing agents or processes which synchronize with each other from time...
Linear-time temporal logic and Büchi automata (1997)
Over the past two decades, temporal logic has become a very basic tool for specifying properties of reactive systems. For finite-state systems, it is possible to use techniques based on Büchi...
Determinizing Asynchronous Automata on Infinite Inputs (1995)
Nils Klarlund, Nils Klarlund, Madhavan Mukund, Madhavan Mukund, Milind Sohoni, Milind Sohoni
is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent publications in the BRICS Report Series. Copies...
[RS-95-54] Abstract, PostScript, DVI. (1995)
Jrgen H. Andersen, Carsten H. Kristensen, Arne Skou Specification, Automated Verification, Real-time Behaviour, Luca Aceto, ...
[RS-95-55] Abstract, PostScript.
Determinizing Asynchronous Automata on Infinite Inputs (1995)
Nils Klarlund, Nils Klarlund, Madhavan Mukund, Madhavan Mukund, Milind Sohoni, Milind Sohoni
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent...
Sohoni: Gossiping, asynchronous automata and Zielonka's theorem, Report TCS-94-2 (1994)
Madhavan Mukund, Milind Sohoni
In this paper, we first tackle a natural problem from distributed computing, involving time-stamps. We then show that our solution to this problem can be applied to provide a simplified proof of...
Determinizing Asynchronous Automata (1993)
Nils Klarlund, Madhavan Mukund, Milind Sohoni
A concurrent version of a finite-state automaton is a set of processes that cooperate in processing letters of the input. Each letter read prompts some of the processes to synchronize and decide on a...
Petri Nets And Step Transition Systems (1992)
Labelled transition systems are a simple yet powerful formalism for describing the operational behaviour of computing systems. They can be extended to model concurrency faithfully by permitting...