Source author record

Amit Kumar Dhar

Amit Kumar Dhar appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Catalog footprint

What is connected

3works
2topics
4close collaborators

Actions

Connect this record

Log in to claim

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

3 published item(s)

preprint2016arXiv

Efficient Energy Distribution in a Smart Grid using Multi-Player Games

Algorithms and models based on game theory have nowadays become prominent techniques for the design of digital controllers for critical systems. Indeed, such techniques enable automatic synthesis: given a model of the environment and a property that the controller must enforce, those techniques automatically produce a correct controller, when it exists. In the present paper, we consider a class of concurrent, weighted, multi-player games that are well-suited to model and study the interactions of several agents who are competing for some measurable resources like energy. We prove that a subclass of those games always admit a Nash equilibrium, i.e. a situation in which all players play in such a way that they have no incentive to deviate. Moreover, the strategies yielding those Nash equilibria have a special structure: when one of the agents deviate from the equilibrium, all the others form a coalition that will enforce a retaliation mechanism that punishes the deviant agent. We apply those results to a real-life case study in which several smart houses that produce their own energy with solar panels, and can share this energy among them in micro-grid, must distribute the use of this energy along the day in order to avoid consuming electricity that must be bought from the global grid. We demonstrate that our theory allows one to synthesise an efficient controller for these houses: using penalties to be paid in the utility bill as an incentive, we force the houses to follow a pre-computed schedule that maximises the proportion of the locally produced energy that is consumed.

preprint2013arXiv

On the Complexity of Verifying Regular Properties on Flat Counter Systems

Among the approximation methods for the verification of counter systems, one of them consists in model-checking their flat unfoldings. Unfortunately, the complexity characterization of model-checking problems for such operational models is not always well studied except for reachability queries or for Past LTL. In this paper, we characterize the complexity of model-checking problems on flat counter systems for the specification languages including first-order logic, linear mu-calculus, infinite automata, and related formalisms. Our results span different complexity classes (mainly from PTime to PSpace) and they apply to languages in which arithmetical constraints on counter values are systematically allowed. As far as the proof techniques are concerned, we provide a uniform approach that focuses on the main issues.

preprint2013arXiv

Taming Past LTL and Flat Counter Systems

Reachability and LTL model-checking problems for flat counter systems are known to be decidable but whereas the reachability problem can be shown in NP, the best known complexity upper bound for the latter problem is made of a tower of several exponentials. Herein, we show that the problem is only NP-complete even if LTL admits past-time operators and arithmetical constraints on counters. Actually, the NP upper bound is shown by adequately combining a new stuttering theorem for Past LTL and the property of small integer solutions for quantifier-free Presburger formulae. Other complexity results are proved, for instance for restricted classes of flat counter systems.