Ashwin Bhaskar

dblp:322/0590 · DBLP profile ↗
← Back
4ranked-venue papers
4as first author
4since 2021 · last 2025
0000-0002-7989-9279ORCID · reported

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 3 · 3 first-author · 3 since 2021Artificial intelligence and machine learning · 1 · 1 first-author · 1 since 2021
YearPublicationVenuePosition
2025 Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications
abstract
When multiple software components interact via method calls, we may want to ensure that the order of invoked methods and the arguments provided adhere to some specification. The classic problem associated with interface automata checks for the existence of a mediator whose intention is to act as a buffer in between method invocations so that invocations do not go unanswered. We extend the base model underlying interface automata, enabling them to exchange integer values - one automaton generates an integer value and outputs it by firing a generating transition and another automaton receives the value by synchronously firing a receiving transition. Transitions in the automata can have guards with linear order constraints on the exchanged values, influencing which methods can or can not be invoked later. So the generated values influence the sequences of invocations that are enabled. We specify desirable properties of the sequence of method calls and the arguments passed to them using an extension of Linear Temporal Logic (LTL). We consider the interoperability problem, which is to check if it is possible to generate integer values in such a way that all enabled sequences satisfy the given specification. We show that the interoperability problem is undecidable in general, even when there are only two participating automata. We show decidability in the case where guards on generating transitions can only have equality constraints on the exchanged value (but receiving transitions can continue to have linear order constraints). We model this problem as a game between two players, one trying to generate integer values such that violating sequences are disabled while the other player tries to dig out violating sequences that are enabled. Interoperability is equivalent to the first player having a winning strategy. We solve this game via a finite abstraction, which results in a symbolic game. We then show that winning strategies for the symbolic game can be translated to winning strategies for the original game over integers.
Ashwin Bhaskar, M. Praveen
FSTTCS1
2024 Realizability problem for constraint LTL
Ashwin Bhaskar, M. Praveen
Inf. Comput.1
2023 Constraint LTL with Remote Access
Ashwin Bhaskar, M. Praveen
FSTTCS1
2022 Realizability Problem for Constraint LTL
Ashwin Bhaskar, M. Praveen
TIME1