Author name cluster

Samik Basu

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.

7 papers

1 author row

AAAI Conference 2025 Conference Paper

Checking Consistency of CP-Theory Preferences in Polynomial Time

Erik Rauer
Samik Basu
Vasant Honavar

We investigate the problem of checking the consistency of qualitative preferences expressed in CP-theory. This problem is PSPACE-Complete even when the preferences are locally consistent or the preference variables have binary domain. We present a new sufficient condition for consistency of preferences and show that the condition can be checked in polynomial time in settings of practical relevance (locally consistent or binary domain preference variables). We further show how the resulting sufficient condition can be used to efficiently identify a subset of outcomes that are non-dominated with respect to a set of qualitative preferences.

PDF Details DOI

IJCAI Conference 2024 Conference Paper

Improved Evolutionary Algorithms for Submodular Maximization with Cost Constraints

Yanhui Zhu
Samik Basu
A. Pavan

We present an evolutionary algorithm evo-SMC for the problem of Submodular Maximization under Cost constraints (SMC). Our algorithm achieves 1/2-approximation with a high probability 1-1/n within O(n2 K) iterations, where K denotes the maximum size of a feasible solution set with cost constraint B. To the best of our knowledge, this is the best approximation guarantee offered by evolutionary algorithms for this problem. We further refine evo-SMC and develop st-evo-SMC. This stochastic version yields a significantly faster algorithm while maintaining the approximation ratio of 1/2, with probability 1-epsilon. The required number of iterations reduces to O(nK log(1/epsilon)/p), where the user defined parameters p represents the stochasticity probability, and epsilon denotes the error threshold. Finally, the empirical evaluations carried out through extensive experimentation substantiate the efficiency and effectiveness of our proposed algorithms. Our algorithms consistently outperform existing methods, producing higher-quality solutions.

PDF Details DOI

TCS Journal 2016 Journal Article

On deciding synchronizability for asynchronously communicating systems

Samik Basu
Tevfik Bultan

Asynchronously communicating systems involve peers or entities that communicate by exchanging messages via buffers. In general, the size of such buffers is not known apriori, i. e. , they are considered to be unbounded. As a result, models of asynchronously communicating systems typically exhibit infinite state spaces and it is well-known that reachability and boundedness problems for such models are undecidable. This, in turn, makes automatic verification of asynchronous systems undecidable as well. We discuss a particular class of asynchronous systems over peers for which the interaction behaviors do not change when the peers are made to communicate synchronously. Such systems are referred to as Synchronizable. Automatic verification of synchronizable systems is decidable as the verification of the system can be performed using its synchronous counterpart. Recently, we have proved that checking whether or not a system is synchronizable is decidable. In this paper, we consider different types of asynchronous communication, where the type is described in terms of the nature of buffering and the number of buffers, and discuss how/if synchronizability is decidable for each type. The new results subsume the existing ones and present a comprehensive synchronizability study of asynchronous systems.

Details DOI

AAAI Conference 2011 Conference Paper

Verifying Intervention Policies to Counter Infection Propagation over Networks: A Model Checking Approach

Ganesh Ram Santhanam
Yuly Suvorov
Samik Basu
Vasant Honavar

Spread of infections (diseases, ideas, etc.) in a network can be modeled as the evolution of states of nodes in a graph as a function of the states of their neighbors. Given an initial conﬁguration of a network in which a subset of the nodes have been infected, and an infection propagation function that speciﬁes how the states of the nodes evolve over time, we show how to use model checking to identify, verify, and evaluate the effectiveness of intervention policies for containing the propagation of infection over such networks. %vspace-0. 1in

PDF Details

AAAI Conference 2010 Conference Paper

Dominance Testing via Model Checking

Ganesh Ram Santhanam
Samik Basu
Vasant Honavar

Dominance testing, the problem of determining whether an outcome is preferred over another, is of fundamental importance in many applications. Hence, there is a need for algorithms and tools for dominance testing. CP-nets and TCP-nets are some of the widely studied languages for representing and reasoning with preferences. We reduce dominance testing in TCP-nets to reachability analysis in a graph of outcomes. We provide an encoding of TCP-nets in the form of a Kripke structure for CTL. We show how to compute dominance using NuSMV, a model checker for CTL. We present results of experiments that demonstrate the feasibility of our approach to dominance testing.

PDF Details

KR Conference 2010 Conference Paper

Efficient Dominance Testing for Unconditional Preferences

Ganesh Ram Santhanam
Samik Basu
Vasant Honavar

We study a dominance relation for comparing outcomes based on unconditional qualitative preferences and compare it with its unconditional counterparts for TCP-nets and their variants. Dominance testing based on this relation can be carried out in polynomial time by evaluating the satisﬁability of a logic formula.

TCS Journal 2006 Journal Article

Compositional analysis for verification of parameterized systems

Samik Basu
C.R. RAMAKRISHNAN

Many safety-critical systems that have been considered by the verification community are parameterized by the number of concurrent components in the system, and hence describe an infinite family of systems. Traditional model checking techniques can only be used to verify specific instances of this family. In this paper, we present a technique based on compositional model checking and program analysis for automatic verification of infinite families of systems. The technique views a parameterized system as an expression in a process algebra (CCS) and interprets this expression over a domain of formulas (modal mu-calculus), considering a process as a property transformer. The transformers are constructed using partial model checking techniques. At its core, our technique solves the verification problem by finding the limit of a chain of formulas. We present a widening operation to find such a limit for properties expressible in a subset of modal mu-calculus. We describe the verification of a number of parameterized systems using our technique to demonstrate its utility.

Details DOI