Carolyn Talcott
Current Organizations / Institutes
The organizations/institutes from the scholar's latest article
Previous Organizations / Institutes
The organizations / institutes from the scholar's other articles in the past ten years
Research Subjects
Carolyn Talcott has a total of 92 co-authors. Here are the top co-authors by number of shared publications:
- Tajana Ban Kirigin
University of Rijeka
10 shared publications - Andre Scedrov
University of Pennsylvania
9 shared publications - Vivek Nigam
Federal University of Paraíba
8 shared publications - Max Kanovich
University College
6 shared publications - Vivek Nigam
Federal University of Paraíba, João Pessoa, Brazil
4 shared publications - Mark-Oliver Stehr
SRI International
3 shared publications
Latest Publications
- 3 October 2022
- Published by Springer Nature
- p. 96-113
On the Formalization and Computational Complexity of Resilience Problems for Cyber-Physical Systems
- 3 October 2022
- Published by Springer Nature
- p. 96-113
On the Formalization and Computational Complexity of Resilience Problems for Cyber-Physical Systems
- 30 July 2022
- Published by Springer Nature
- p. 212-229
Automating Safety Proofs About Cyber-Physical Systems Using Rewriting Modulo SMT
- 30 July 2022
- Published by Springer Nature
- p. 212-229
Automating Safety Proofs About Cyber-Physical Systems Using Rewriting Modulo SMT
- 2 July 2022
- Published by Springer Nature in SN Computer Science
- Vol. 3 (5) , 1-22
On the Security and Complexity of Periodic Systems
- 2 July 2022
- Published by Springer Nature in SN Computer Science
- Vol. 3 (5) , 1-22
On the Security and Complexity of Periodic Systems
- Open Access
On the Complexity of Verification of Time-Sensitive Distributed Systems: Technical Report
This paper develops a Multiset Rewriting language with explicit time for the specification and analysis of Time-Sensitive Distributed Systems (TSDS). Goals are often specified using explicit time constraints. A good trace is an infinite trace in which the goals are satisfied perpetually despite possible interference from the environment. In our previous work (FORMATS 2016), we discussed two desirable properties of TSDSes, realizability (there exists a good trace) and survivability (where, in addition, all admissible traces are good). Here we consider two additional properties, recoverability (all compliant traces do not reach points-of-no-return) and reliability (the system can always continue functioning using a good trace). Following (FORMATS 2016), we focus on a class of systems called Progressing Timed Systems (PTS), where intuitively only a finite number of actions can be carried out in a bounded time period. We prove that for this class of systems the properties of recoverability and reliability coincide and are PSPACE-complete. Moreover, if we impose a bound on time (as in bounded model-checking), we show that for PTS the reliability property is in the $\Pi_2^p$ class of the polynomial hierarchy, a subclass of PSPACE. We also show that the bounded survivability is both NP-hard and coNP-hard.Open AccessOn the Complexity of Verification of Time-Sensitive Distributed Systems: Technical Report
This paper develops a Multiset Rewriting language with explicit time for the specification and analysis of Time-Sensitive Distributed Systems (TSDS). Goals are often specified using explicit time constraints. A good trace is an infinite trace in which the goals are satisfied perpetually despite possible interference from the environment. In our previous work (FORMATS 2016), we discussed two desirable properties of TSDSes, realizability (there exists a good trace) and survivability (where, in addition, all admissible traces are good). Here we consider two additional properties, recoverability (all compliant traces do not reach points-of-no-return) and reliability (the system can always continue functioning using a good trace). Following (FORMATS 2016), we focus on a class of systems called Progressing Timed Systems (PTS), where intuitively only a finite number of actions can be carried out in a bounded time period. We prove that for this class of systems the properties of recoverability and reliability coincide and are PSPACE-complete. Moreover, if we impose a bound on time (as in bounded model-checking), we show that for PTS the reliability property is in the $\Pi_2^p$ class of the polynomial hierarchy, a subclass of PSPACE. We also show that the bounded survivability is both NP-hard and coNP-hard. - 28 April 2019
- Published by Springer Nature in Lecture Notes in Computer Science
- p. 192-213
A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols
- 28 April 2019
- Published by Springer Nature in Lecture Notes in Computer Science
- p. 192-213
A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols
- 28 April 2019
- Published by Springer Nature in Lecture Notes in Computer Science
- p. 89-111
Symbolic Timed Trace Equivalence
- 28 April 2019
- Published by Springer Nature in Lecture Notes in Computer Science
- p. 89-111
Symbolic Timed Trace Equivalence
- Open Access
Symbolic Timed Observational Equivalence
Intruders can infer properties of a system by measuring the time it takes for the system to respond to some request of a given protocol, that is, by exploiting time side channels. These properties may help intruders distinguish whether a system is a honeypot or concrete system helping him avoid defense mechanisms, or track a user among others violating his privacy. Observational equivalence is the technical machinery used for verifying whether two systems are distinguishable. Moreover, efficient symbolic methods have been developed for automating the check of observational equivalence of systems. This paper introduces a novel definition of timed observational equivalence which also distinguishes systems according to their time side channels. Moreover, as our definition uses symbolic time constraints, it can be automated by using SMT-solvers.
Open AccessSymbolic Timed Observational Equivalence
Intruders can infer properties of a system by measuring the time it takes for the system to respond to some request of a given protocol, that is, by exploiting time side channels. These properties may help intruders distinguish whether a system is a honeypot or concrete system helping him avoid defense mechanisms, or track a user among others violating his privacy. Observational equivalence is the technical machinery used for verifying whether two systems are distinguishable. Moreover, efficient symbolic methods have been developed for automating the check of observational equivalence of systems. This paper introduces a novel definition of timed observational equivalence which also distinguishes systems according to their time side channels. Moreover, as our definition uses symbolic time constraints, it can be automated by using SMT-solvers.
- Open Access
Compliance in Real Time Multiset Rewriting Models
The notion of compliance in Multiset Rewriting Models (MSR) has been introduced for untimed models and for models with discrete time. In this paper we revisit the notion of compliance and adapt it to fit with additional nondeterminism specific for dense time domains. Existing MSR with dense time are extended with critical configurations and non-critical traces, that is, traces involving no critical configurations. Complexity of related {\em non-critical reachability problem} is investigated. Although this problem is undecidable in general, we prove that for balanced MSR with dense time the non-critical reachability problem is PSPACE-complete.
Open AccessCompliance in Real Time Multiset Rewriting Models
The notion of compliance in Multiset Rewriting Models (MSR) has been introduced for untimed models and for models with discrete time. In this paper we revisit the notion of compliance and adapt it to fit with additional nondeterminism specific for dense time domains. Existing MSR with dense time are extended with critical configurations and non-critical traces, that is, traces involving no critical configurations. Complexity of related {\em non-critical reachability problem} is investigated. Although this problem is undecidable in general, we prove that for balanced MSR with dense time the non-critical reachability problem is PSPACE-complete.