Showing 1–2 of 2 results for author: Thiagarajan, P S
-
LPrL: An Asynchronous Linear Time Hyper Logic
Authors:
Parasara Sridhar Duggirala,
P. S. Thiagarajan
Abstract:
We present a novel asynchronous hyper linear time temporal logic named LPrL (Linear Time Predicate Logic) and establish its basic theory. LPrL is a natural first order extension of LTL (Linear time temporal logic), in which the predicates specify the properties of and the relationships between traces (infinite sequences of actions) using Boolean combinations of LTL formulas. To augment the express…
▽ More
We present a novel asynchronous hyper linear time temporal logic named LPrL (Linear Time Predicate Logic) and establish its basic theory. LPrL is a natural first order extension of LTL (Linear time temporal logic), in which the predicates specify the properties of and the relationships between traces (infinite sequences of actions) using Boolean combinations of LTL formulas. To augment the expressive power of the logic, we introduce a simple language of terms and add the equality predicate t = t' where t and t' are terms. We first illustrate how a number of the security policies as well as a basic consistency property of distributed processes can be captured using LPrL. We then establish our main results using automata theoretic techniques. Namely, the satisfiability and model checking problems for LPrL can be solved in elementary time. These results are in sharp contrast to HyperLTL, the prevalent synchronous hyper linear time logic, whose satisfiability problem is undecidable and whose model checking problem has non-elementary time complexity.
△ Less
Submitted 29 May, 2025; v1 submitted 10 May, 2025;
originally announced May 2025.
-
Distributed Markov Chains
Authors:
Sumit Kumar Jha,
Madhavan Mukund,
Ratul Saha,
P S Thiagarajan
Abstract:
The formal verification of large probabilistic models is important and challenging. Exploiting the concurrency that is often present is one way to address this problem. Here we study a restricted class of asynchronous distributed probabilistic systems in which the synchronizations determine the probability distribution for the next moves of the participating agents. The key restriction we impose i…
▽ More
The formal verification of large probabilistic models is important and challenging. Exploiting the concurrency that is often present is one way to address this problem. Here we study a restricted class of asynchronous distributed probabilistic systems in which the synchronizations determine the probability distribution for the next moves of the participating agents. The key restriction we impose is that the synchronizations are deterministic, in the sense that any two simultaneously enabled synchronizations must involve disjoint sets of agents. As a result, this network of agents can be viewed as a succinct and distributed presentation of a large global Markov chain. A rich class of Markov chains can be represented this way.
We define an interleaved semantics for our model in terms of the local synchronization actions. The network structure induces an independence relation on these actions, which, in turn, induces an equivalence relation over the interleaved runs in the usual way. We construct a natural probability measure over these equivalence classes of runs by exploiting Mazurkiewicz trace theory and the probability measure space of the associated global Markov chain.
It turns out that verification of our model, called DMCs (distributed Markov chains), can often be efficiently carried out by exploiting the partial order nature of the interleaved semantics. To demonstrate this, we develop a statistical model checking (SMC) procedure and use it to verify two large distributed probabilistic networks.
△ Less
Submitted 5 August, 2014;
originally announced August 2014.
