skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


Title: Generation of Minimum Tree-Like Witnesses for Existential CTL
An advantage of model checking is its ability to generate witnesses or counterexamples. Approaches exist to generate small or minimum witnesses for simple unnested formulas, but no existing method guarantees minimality for general nested ones. Here, we give a definition of witness size, use edge-valued decision diagrams to recursively compute the minimum witness size for each subformula, and describe a general approach to build minimum tree-like witnesses for existential CTL. Experimental results show that for some models, our approach is able to generate minimum witnesses while the traditional approach is not.  more » « less
Award ID(s):
1642397
PAR ID:
10082409
Author(s) / Creator(s):
;
Date Published:
Journal Name:
Tools and Algorithms for the Construction and Analysis of Systems
Page Range / eLocation ID:
328--343
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; (, Child Abuse & Neglect)
    Background: Adolescents frequently experience and witness violence and crime, yet very little research has been conducted to determine how best to question these witnesses to elicit complete and accurate disclosures. Objective: This systematic review integrated scientific research on rapport building with child and adult witnesses with theory and research on adolescent development in order to identify rapport building techniques likely to be effective with suspected adolescent victims and witnesses. Method: Four databases were searched to identify investigations of rapport building in forensic interviewing of adolescents. Results: Despite decades of research of studies including child and adult participants, only one study since 1990 experimentally tested techniques to build rapport with adolescents. Most rapport strategies used with children and adults have yet to be tested with adolescents. Tests of these strategies, along with modifications based on developmental science of adolescence, would provide a roadmap to determining which approaches are most beneficial when questioning adolescent victims and witnesses. Conclusions: There is a clear need for research that tests what strategies are best to use with adolescents. They may be reluctant to disclose information about stressful or traumatic experi- ences to adults due to both normative developmental processes and the types of events about which they are questioned in legal settings. Rapport building approaches tailored to address adolescents’ motivational needs may be effective in increasing adolescents’ reporting, and additional research testing such approaches will provide much-needed insight to inform the development of evidence-based practices for questioning these youth 
    more » « less
  2. ; ; (, Child abuse and neglect)
    Background: Adolescents frequently experience and witness violence and crime, yet very little research has been conducted to determine how best to question these witnesses to elicit complete and accurate disclosures. Objective: This systematic review integrated scientific research on rapport building with child and adult witnesses with theory and research on adolescent development in order to identify rapport building techniques likely to be effective with suspected adolescent victims and witnesses. Method: Four databases were searched to identify investigations of rapport building in forensic interviewing of adolescents. Results: Despite decades of research of studies including child and adult participants, only one study since 1990 experimentally tested techniques to build rapport with adolescents. Most rapport strategies used with children and adults have yet to be tested with adolescents. Tests of these strategies, along with modifications based on developmental science of adolescence, would provide a roadmap to determining which approaches are most beneficial when questioning adolescent victims and witnesses. Conclusions: There is a clear need for research that tests what strategies are best to use with adolescents. They may be reluctant to disclose information about stressful or traumatic experiences to adults due to both normative developmental processes and the types of events about which they are questioned in legal settings. Rapport building approaches tailored to address adolescents’ motivational needs may be effective in increasing adolescents’ reporting, and additional research testing such approaches will provide much-needed insight to inform the development of evidence-based practices for questioning these youth. 
    more » « less
  3. ; (, Annual International Cryptology Conference)
    We initiate the study of witness authenticating NIZK proof systems (waNIZKs), in which one can use a witness w of a statement x to identify whether a valid proof for x is indeed generated using w. Such a new identification functionality enables more diverse applications, and it also puts new requirements on soundness that: (1) no adversary can generate a valid proof that will not be identified by any witness; (2) or forge a proof using her valid witness to frame others. To work around the obvious obstacle towards conventional zero-knowledgeness, we define entropic zero-knowledgeness that requires the proof to leak no partial information, if the witness has sufficient computational entropy. We give a formal treatment of this new primitive. The modeling turns out to be quite involved and multiple subtle points arise and particular cares are required. We present general constructions from standard assumptions. We also demonstrate three applications in non-malleable (perfectly one-way) hash, group signatures with verifier-local revocations and plaintext-checkable public-key encryption. Our waNIZK provides a new tool to advance the state of the art in all these applications. 
    more » « less
  4. ; ; ; (, IEEE International Conference on Data Mining Workshops)
    null (Ed.)
    Homicide investigations generate large and diverse data in the form of witness interview transcripts, physical evidence, photographs, DNA, etc. Homicide case chronologies are summaries of these data created by investigators that consist of short text-based entries documenting specific steps taken in the investigation. A chronology tracks the evolution of an investigation, including when and how persons involved and items of evidence became part of a case. In this article we discuss a framework for creating knowledge graphs of case chronologies that may aid investigators in analyzing homicide case data and also allow for post hoc analysis of the key features that determine whether a homicide is ultimately solved. Our method consists of 1) performing named entity recognition to determine witnesses, suspects, and detectives from chronology entries 2) using keyword expansion to identify documentary, physical, and forensic evidence in each entry and 3) linking entities and evidence to construct a homicide investigation knowledge graph. We compare the performance of several choices of methodologies for these sub-tasks using homicide investigation chronologies from Los Angeles, California. We then analyze the association between network statistics of the knowledge graphs and homicide solvability. 
    more » « less
  5. ; ; ; (, Mathematics of Computation)
    null (Ed.)
    A numerical description of an algebraic subvariety of projective space is given by a general linear section, called a witness set. For a subvariety of a product of projective spaces (a multiprojective variety), the corresponding numerical description is given by a witness collection, whose structure is more involved. We build on recent work to develop a toolkit for the numerical manipulation of multiprojective varieties that operates on witness collections and to use this toolkit in an algorithm for numerical irreducible decomposition of multiprojective varieties. The toolkit and decomposition algorithm are illustrated throughout in a series of examples. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email