In the context of information systems, text sanitization techniques are used to identify and remove sensitive data to comply with security and regulatory requirements. Even though many methods for privacy preservation have been proposed, most of them are focused on the detection of entities from specific domains (e.g., credit card numbers, social security numbers), lacking generality and requiring customization for each desirable domain. Moreover, removing words is, in general, a drastic measure, as it can degrade text coherence and contextual information. Less severe measures include substituting a word for a safe alternative, yet it can be challenging to automatically find meaningful substitutions. We present a zero-shot text sanitization technique that detects and substitutes potentially sensitive information using Large Language Models. Our evaluation shows that our method excels at protecting privacy while maintaining text coherence and contextual information, preserving data utility for downstream tasks.

We study directed control of discrete event system expressed as the parallel composition of interacting automata. Solutions that first compose the automata and then compute a controller may result in an exponential blow up. We present a technique that builds the composition on-the-fly guided by a novel domain-independent heuristic, which attempts to discover relevant dependencies between the intervening components. We obtain safe and non-blocking directed controllers, or directors, exploring a reduced portion of the state space. We present the first experimental results on directed control comparing on-the-fly composition with informed search against the original monolithic approach to directed control.

A planning domain, as any model, is never “complete” and inevitably makes assumptions on the environment's dynamic. By allowing the specification of just one domain model, the knowledge engineer is only able to make one set of assumptions, and to specify a single objective-goal. Borrowing from work in Software Engineering, we propose a multi-tier framework for planning that allows the specification of different sets of assumptions, and of different corresponding objectives. The framework aims to support the synthesis of adaptive behavior so as to mitigate the intrinsic risk in any planning modeling task. After defining the multi-tier planning task and its solution concept, we show how to solve problem instances by a succinct compilation to a form of non-deterministic planning. In doing so, our technique justifies the applicability of planning with both fair and unfair actions, and the need for more efforts in developing planning systems supporting dual fairness assumptions.

We show how reactive synthesis and automated planning can be leveraged effectively to find nonmaximal solutions to deterministic supervisory control problems of discrete event systems. To do so, we propose efficient translations of the supervisory control problem into the reactive synthesis and planning frameworks. Notably, our translation methods capture the compositional and reactive nature of control specifications, avoiding a potential exponential explosion found in alternative translation approaches. Additionally, we report on experimental results comparing the efficacy of different tools from the three disciplines, for a particular supervisory control benchmark.

The problem of automatically constructing a software component such that when executed in a given environment satisfies a goal, is recurrent in software engineering. Controller synthesis is a field which fits into this vision. In this paper we study controller synthesis for partially observable LTS models. We exploit the link between partially observable control and non-determinism and show that, unlike fully observable LTS or Kripke structure control problems, in this setting the existence of a solution depends on the interaction model between the controller-to-be and its environment. We identify two interaction models, namely Interface Automata and Weak Interface Automata, define appropriate control problems and describe synthesis algorithms for each of them.

This paper presents a Directed Controller Synthesis (DCS) technique for discrete event systems. This DCS method explores the solution space for reactive controllers guided by a domain-independent heuristic. The heuristic is derived from an efficient abstraction of the environment based on the componentized way in which complex environments are described. Then by building the composition of the components on-the-fly DCS obtains a solution by exploring a reduced portion of the state space. This work focuses on untimed discrete event systems with safety and co-safety (i.e. reachability) goals. An evaluation for the technique is presented comparing it to other well-known approaches to controller synthesis (based on symbolic representation and compositional analyses).

This paper presents a Directed Controller Synthesis (DCS) technique for discrete event systems. The DCS method explores the solution space for reactive controllers guided by a domain-independent heuristic. The heuristic is derived from an efficient abstraction of the environment based on the componentized way in which complex environments are described. Then by building the composition of the components on-the-fly DCS obtains a solution by exploring a reduced portion of the state space. This work focuses on untimed discrete event systems with safety and co-safety (i.e. reachability) goals. An evaluation for the technique is presented comparing it to other well-known approaches to controller synthesis (based on symbolic representation and compositional analyses).

SUMMARYTranslation of Annotated COde (TACO) is a SAT‐based tool for bounded verification of Java programs. One challenge many formal tools share is to provide a practical interface for a non‐proficient user. In this article, we present an Eclipse plug‐in for the static verifier TACO. This plug‐in allows a user to walk a counterexample trace mimicking a debugging session. TacoPlug (our plug‐in) uses and extends TACO to provide a better debugging experience. TacoPlug interface allows the user to verify an annotated software using the TACO verifier. If TACO finds a violation to the specification, TacoPlug presents it in terms of the annotated source code. TacoPlug features several views of the error trace to facilitate fault understanding. It resembles any software debugger, but the debugging occurs statically without executing the program. Furthermore, should a dynamic analysis be required, TacoPlug presents the user with a unit test case generated by TACO based on the detected violation. We show the usability of our tool by means of a motivational example taken from a real‐life software error. Copyright © 2013 John Wiley & Sons, Ltd.

We present a novel and general technique for automated test generation that combines tight bounds with incremental SAT solving. The proposed technique uses incremental SAT to build test suites targeting a specific testing criterion, amongst various black-box and white-box criteria. As our experimental results show, the combination of tight bounds with incremental SAT, and the testing criterion driven approach implemented in our prototype tool FAJITA, enable us to effectively generate test suites for container classes with rich contracts, more efficiently than other state-of-the-art tools.